theory Ipc_R

lemma reply_cap_end_mdb_chain:
  "\<lbrakk> cte_wp_at (is_reply_cap_to t) slot s; invs s;
     invs' s';
     (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte \<rbrakk>
      \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer
            \<and> mdbNext (cteMDBNode cte) = nullPointer)
           \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte))
                    (mdbPrev (cteMDBNode cte)) s'" apply (clarsimp simp only: cte_wp_at_reply_cap_to_ex_rights) apply (frule(1) pspace_relation_ctes_ofI[OF state_relation_pspace_relation],
         clarsimp+) apply (subgoal_tac "\<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights')
                          \<and> descendants_of slot' (cdt s) = {slot}") apply (elim state_relationE exE) apply (clarsimp simp: cdt_relation_def
               simp del: split_paired_All) apply (drule spec, drule(1) mp[OF _ caps_of_state_cte_at]) apply (frule(1) pspace_relation_cte_wp_at[OF _ caps_of_state_cteD],
          clarsimp+) apply (clarsimp simp: descendants_of'_def cte_wp_at_ctes_of) apply (frule_tac f="\<lambda>S. cte_map slot \<in> S" in arg_cong, simp(no_asm_use)) apply (frule invs_mdb'[unfolded valid_mdb'_def]) apply (rule context_conjI) apply (clarsimp simp: nullPointer_def valid_mdb_ctes_def) apply (erule(4) subtree_prev_0) apply (rule conjI) apply (rule ccontr) apply (frule valid_mdb_no_loops, simp add: no_loops_def) apply (drule_tac x="cte_map slot" in spec) apply (erule notE, rule r_into_trancl, rule ccontr) apply (clarsimp simp: mdb_next_unfold valid_mdb_ctes_def nullPointer_def) apply (rule valid_dlistEn, assumption+) apply (subgoal_tac "ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)") apply (frule(3) class_linksD) apply (clarsimp simp: isCap_simps dest!: capClass_Reply[OF sym]) apply (drule_tac f="\<lambda>S. mdbNext (cteMDBNode cte) \<in> S" in arg_cong) apply (simp, erule notE, rule subtree.trans_parent, assumption+) apply (case_tac ctea, case_tac cte') apply (clarsimp simp add: parentOf_def isMDBParentOf_CTE) apply (simp add: sameRegionAs_def2 isCap_simps) apply (erule subtree.cases) apply (clarsimp simp: parentOf_def isMDBParentOf_CTE) apply (clarsimp simp: parentOf_def isMDBParentOf_CTE) apply (simp add: mdb_next_unfold) apply (erule subtree.cases) apply (clarsimp simp: valid_mdb_ctes_def) apply (erule_tac cte=ctea in valid_dlistEn, assumption) apply (simp add: mdb_next_unfold) apply (clarsimp simp: mdb_next_unfold isCap_simps) apply (drule_tac f="\<lambda>S. c' \<in> S" in arg_cong) apply (clarsimp simp: no_loops_direct_simp valid_mdb_no_loops) apply (frule invs_mdb) apply (drule invs_valid_reply_caps) apply (clarsimp simp: valid_mdb_def reply_mdb_def
                        valid_reply_caps_def reply_caps_mdb_def
                        cte_wp_at_caps_of_state
              simp del: split_paired_All) apply (erule_tac x=slot in allE, erule_tac x=t in allE, erule impE, fast) apply (elim exEI) apply clarsimp apply (subgoal_tac "P" for P, rule sym, rule equalityI, assumption) apply clarsimp apply (erule(4) unique_reply_capsD) apply (simp add: descendants_of_def) apply (rule r_into_trancl) apply (simp add: cdt_parent_rel_def is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_reply_cap_to t) slot s; invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer) \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s' proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer) \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s' proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s' proof (prove)
goal (2 subgoals):
 1. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot}\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s'
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights slot' rights'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot}\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s'
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s'
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; cte_map ` descendants_of (a, b) (cdt s) = descendants_of' (cte_map (a, b)) (ctes_of s')\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s'
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = descendants_of' (cte_map (a, b)) (ctes_of s'); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t True (AllowGrant \<in> rights')) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) (mdbPrev (cteMDBNode cte)) s'
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights')\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s')\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s')\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); mdbPrev (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = nullPointer \<and> (\<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea))
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = nullPointer
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; mdbNext (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; mdbNext (cteMDBNode cte) \<noteq> nullPointer; \<forall>c. (c, c) \<notin> (mdb_next_rel (ctes_of s'))\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; mdbNext (cteMDBNode cte) \<noteq> nullPointer; (cte_map slot, cte_map slot) \<notin> (mdb_next_rel (ctes_of s'))\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; mdbNext (cteMDBNode cte) \<noteq> nullPointer; (cte_map slot, cte_map slot) \<notin> mdb_next_rel (ctes_of s')\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s')\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte' v1 v2. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = Collect (subtree (ctes_of s') (cte_map (a, b))); ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cteCap cte' = capability.ReplyCap t v1 v2\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte' v1 v2. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cteCap cte' = capability.ReplyCap t v1 v2; (mdbNext (cteMDBNode cte) \<in> {cte_map slot}) = (mdbNext (cteMDBNode cte) \<in> Collect (subtree (ctes_of s') (cte_map (a, b))))\<rbrakk> \<Longrightarrow> False
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte' v1 v2. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cteCap cte' = capability.ReplyCap t v1 v2\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a, b) parentOf mdbNext (cteMDBNode cte)
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea cte' v1 v2 x1 x2 x1a x2a. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cteCap cte' = capability.ReplyCap t v1 v2; ctea = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map (a, b) parentOf mdbNext (cteMDBNode cte)
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' v1 v2 x2 x2a. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some (CTE (capability.ReplyCap t True (AllowGrant \<in> rights')) x2); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some (CTE (capability.ReplyCap t v1 v2) x2a); mdbPrev x2a = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> global.sameRegionAs (capability.ReplyCap t True (AllowGrant \<in> rights')) (capability.ReplyCap t v1 v2) \<and> mdbRevocable x2
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' v1 v2 x2 x2a. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some (CTE (capability.ReplyCap t True (AllowGrant \<in> rights')) x2); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some (CTE (capability.ReplyCap t v1 v2) x2a); mdbPrev x2a = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> mdbRevocable x2
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (5 subgoals):
 1. \<And>rights a b rights' v1 v2 x2 x2a c'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some (CTE (capability.ReplyCap t True (AllowGrant \<in> rights')) x2); mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some (CTE (capability.ReplyCap t v1 v2) x2a); mdbPrev x2a = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cte_map slot = c'; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> c'; c' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c'\<rbrakk> \<Longrightarrow> mdbRevocable x2
 2. \<And>rights a b rights' v1 v2 x2 x2a c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some (CTE (capability.ReplyCap t True (AllowGrant \<in> rights')) x2); mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some (CTE (capability.ReplyCap t v1 v2) x2a); mdbPrev x2a = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> mdbRevocable x2
 3. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 4. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 5. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' v1 v2 x2 x2a c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some (CTE (capability.ReplyCap t True (AllowGrant \<in> rights')) x2); mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some (CTE (capability.ReplyCap t v1 v2) x2a); mdbPrev x2a = cte_map slot; ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte); cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> mdbRevocable x2
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 3. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cte_map slot \<noteq> mdbNext (cteMDBNode cte); valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map slot\<rbrakk> \<Longrightarrow> ctes_of s' \<turnstile> cte_map slot \<leadsto> mdbNext (cteMDBNode cte)
 2. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> cte_map slot; valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea c'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c'; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> c'; c' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c'\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = Collect (subtree (ctes_of s') (cte_map (a, b))); ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> cte_map slot; cte_map slot \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf cte_map slot; valid_dlist (ctes_of s'); no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s')\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (4 subgoals):
 1. \<And>rights a b rights' ctea. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = Collect (subtree (ctes_of s') (cte_map (a, b))); ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> cte_map slot; cte_map slot \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf cte_map slot; no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s')\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) \<noteq> 0
 2. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = Collect (subtree (ctes_of s') (cte_map (a, b))); ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> cte_map slot; cte_map slot \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf cte_map slot; no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map (a, b)\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 4. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (3 subgoals):
 1. \<And>rights a b rights' ctea cte'. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = Collect (subtree (ctes_of s') (cte_map (a, b))); ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; ctes_of s' \<turnstile> cte_map (a, b) \<leadsto> cte_map slot; cte_map slot \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf cte_map slot; no_0 (ctes_of s'); mdb_chain_0 (ctes_of s'); valid_badges (ctes_of s'); caps_contained' (ctes_of s'); mdb_chunked (ctes_of s'); untyped_mdb' (ctes_of s'); untyped_inc' (ctes_of s'); valid_nullcaps (ctes_of s'); ut_revocable' (ctes_of s'); class_links (ctes_of s'); distinct_zombies (ctes_of s'); irq_control (ctes_of s'); reply_masters_rvk_fb (ctes_of s'); ctes_of s' (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode cte') = cte_map (a, b)\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 3. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; {cte_map slot} = {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights a b rights' ctea c' c''. \<lbrakk>invs s; invs' s'; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'); descendants_of (a, b) (cdt s) = {slot}; ctes_of s' (cte_map (a, b)) = Some ctea; cteCap ctea = capability.ReplyCap t True (AllowGrant \<in> rights'); valid_mdb_ctes (ctes_of s'); mdbPrev (cteMDBNode cte) \<noteq> nullPointer; cte_map slot = c''; ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> cte_map (a, b) parentOf c''; (c' \<in> {cte_map slot}) = (c' \<in> {c'. ctes_of s' \<turnstile> cte_map (a, b) \<rightarrow> c'})\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s' (mdbPrev (cteMDBNode cte)) = Some ctea \<and> isReplyCap (cteCap ctea) \<and> capReplyMaster (cteCap ctea)
 2. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights)\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs s; invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); valid_mdb s\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; cte_wp_at ((=) (cap.ReplyCap t False rights)) slot s; cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); valid_mdb s; valid_reply_caps s\<rbrakk> \<Longrightarrow> \<exists>slot' rights'. caps_of_state s slot' = Some (cap.ReplyCap t True rights') \<and> descendants_of slot' (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); \<forall>ptr t. (\<exists>rights. caps_of_state s ptr = Some (cap.ReplyCap t False rights)) \<longrightarrow> (\<exists>a b. cdt s ptr = Some (a, b) \<and> (\<exists>rights'. caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'))); reply_masters_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>rights'. caps_of_state s (a, b) = Some (cap.ReplyCap t True rights')) \<and> descendants_of (a, b) (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); \<exists>a b. cdt s slot = Some (a, b) \<and> (\<exists>rights'. caps_of_state s (a, b) = Some (cap.ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> \<exists>a b. (\<exists>rights'. caps_of_state s (a, b) = Some (cap.ReplyCap t True rights')) \<and> descendants_of (a, b) (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights x xa. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa) \<and> (\<exists>rights'. caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> (\<exists>rights'. caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')) \<and> descendants_of (x, xa) (cdt s) = {slot} proof (prove)
goal (1 subgoal):
 1. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> descendants_of (x, xa) (cdt s) = {slot} proof (prove)
goal (2 subgoals):
 1. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights'); {slot} \<subseteq> descendants_of (x, xa) (cdt s)\<rbrakk> \<Longrightarrow> descendants_of (x, xa) (cdt s) \<subseteq> {slot}
 2. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> {slot} \<subseteq> descendants_of (x, xa) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>rights x xa rights' a b. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights'); slot \<in> descendants_of (x, xa) (cdt s); (a, b) \<in> descendants_of (x, xa) (cdt s)\<rbrakk> \<Longrightarrow> (a, b) = slot
 2. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> {slot} \<subseteq> descendants_of (x, xa) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> {slot} \<subseteq> descendants_of (x, xa) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> (x, xa) \<rightarrow> slot proof (prove)
goal (1 subgoal):
 1. \<And>rights x xa rights'. \<lbrakk>invs' s'; (s, s') \<in> state_relation; ctes_of s' (cte_map slot) = Some cte; caps_of_state s slot = Some (cap.ReplyCap t False rights); cteCap cte = capability.ReplyCap t False (AllowGrant \<in> rights); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); \<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_masters_mdb (cdt s) (caps_of_state s); cdt s slot = Some (x, xa); caps_of_state s (x, xa) = Some (cap.ReplyCap t True rights')\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> (x, xa) \<leadsto> slot proof (prove)
goal:
No subgoals!