theory CNodeInv_R

lemma cap_revoke_mdb_stuff4:
  "\<lbrakk> (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s;
     cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s';
     cap \<noteq> cap.NullCap; cteCap cte \<noteq> NullCap;
     descendants_of p (cdt s) \<noteq> {} \<rbrakk>
     \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p'
         \<and> next_child p (cdt_list s) = Some p'" apply(subgoal_tac "descendants_of p (cdt s) \<noteq> {}") prefer 2 apply simp apply (subst(asm) cap_revoke_mdb_stuff1) apply assumption+ apply (clarsimp simp: cte_wp_at_ctes_of state_relation_def) apply (drule(1) pspace_relation_cte_wp_atI[where x="mdbNext c" for c]) apply clarsimp apply clarsimp apply (intro exI, rule conjI [OF refl]) apply(simp add: cdt_list_relation_def) apply(erule_tac x="fst p" in allE, erule_tac x="snd p" in allE) apply(case_tac "cte", simp) apply(case_tac "next_slot p (cdt_list s) (cdt s)") apply(simp add: next_slot_def empty_list_empty_desc next_child_None_empty_desc) apply(frule cte_at_next_slot') apply(erule invs_mdb) apply(simp add: invs_def valid_state_def finite_depth) apply(assumption) apply(simp add: next_slot_def empty_list_empty_desc) apply(frule invs_valid_pspace, simp add: valid_pspace_def) apply(rule cte_map_inj_eq) apply(simp add: cte_wp_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p'
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) \<noteq> {}
 2. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> (s, ?s'1) \<in> state_relation
 2. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) ?cap1) p s
 3. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) ?cte1) (cte_map p) ?s'1
 4. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> invs s
 5. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> invs' ?s'1
 6. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ?cap1 \<noteq> cap.NullCap
 7. \<lbrakk>descendants_of p (cdt s) \<noteq> {}; (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cteCap ?cte1 \<noteq> capability.NullCap
 8. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; \<not> \<not> (mdbNext (cteMDBNode ?cte1) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf ?cte1) (mdbNext (cteMDBNode ?cte1)) ?s'1); descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; \<not> \<not> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<and> cte_wp_at' (isMDBParentOf cte) (mdbNext (cteMDBNode cte)) s'); descendants_of p (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. mdbNext (cteMDBNode cte) = cte_map p' \<and> next_child p (cdt_list s) = Some p' proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; pspace_relation (kheap s) (ksPSpace s'); mdbNext (cteMDBNode cte) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'\<rbrakk> \<Longrightarrow> \<exists>a b. mdbNext (cteMDBNode cte) = cte_map (a, b) \<and> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>ctea. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; mdbNext (cteMDBNode cte) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>ctea. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; mdbNext (cteMDBNode cte) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap ctea) \<and> mdbNext (cteMDBNode cte) = cte_map slot\<rbrakk> \<Longrightarrow> \<exists>a b. mdbNext (cteMDBNode cte) = cte_map (a, b) \<and> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; mdbNext (cteMDBNode cte) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap ctea) \<and> mdbNext (cteMDBNode cte) = cte_map slot\<rbrakk> \<Longrightarrow> \<exists>a b. mdbNext (cteMDBNode cte) = cte_map (a, b) \<and> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext (cteMDBNode cte) = cte_map (a, b)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_map (a, b) = cte_map (aa, ba) \<and> next_child p (cdt_list s) = Some (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf cte ctea; 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'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext (cteMDBNode cte) = cte_map (a, b)\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf cte ctea; 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'); \<forall>a b cap node. ctes_of s' (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> (case next_slot (a, b) (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext (cteMDBNode cte) = cte_map (a, b)\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some cte; invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; cteCap cte \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf cte ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext (cteMDBNode cte) = cte_map (a, b); \<forall>cap node. ctes_of s' (cte_map (fst p, snd p)) = Some (CTE cap node) \<longrightarrow> (case next_slot (fst p, snd p) (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next)\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b x1 x2. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>ctea c a b x1 x2. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b)
 2. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (4 subgoals):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> finite_depth (cdt s)
 3. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> next_slot (?p43 ctea c a b x1 x2 aa) (cdt_list s) (cdt s) = Some (?n43 ctea c a b x1 x2 aa)
 4. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa; cte_wp_at (\<lambda>_. True) (?n43 ctea c a b x1 x2 aa) s\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (3 subgoals):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> finite_depth (cdt s)
 2. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> next_slot (?p43 ctea c a b x1 x2 aa) (cdt_list s) (cdt s) = Some (?n43 ctea c a b x1 x2 aa)
 3. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa; cte_wp_at (\<lambda>_. True) (?n43 ctea c a b x1 x2 aa) s\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa\<rbrakk> \<Longrightarrow> next_slot (?p43 ctea c a b x1 x2 aa) (cdt_list s) (cdt s) = Some (?n43 ctea c a b x1 x2 aa)
 2. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa; cte_wp_at (\<lambda>_. True) (?n43 ctea c a b x1 x2 aa) s\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map (a, b) \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map (a, b)) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map (a, b); case next_slot p (cdt_list s) (cdt s) of None \<Rightarrow> True | Some next \<Rightarrow> cte_map (a, b) = cte_map next; cte = CTE x1 x2; next_slot p (cdt_list s) (cdt s) = Some aa; cte_wp_at (\<lambda>_. True) aa s\<rbrakk> \<Longrightarrow> next_child p (cdt_list s) = Some (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s\<rbrakk> \<Longrightarrow> aa = (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> aa = (a, b) proof (prove)
goal (6 subgoals):
 1. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> cte_map aa = cte_map (a, b)
 2. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) aa (?s51 ctea c a b x1 x2 aa)
 3. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) (?s51 ctea c a b x1 x2 aa)
 4. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> valid_objs (?s51 ctea c a b x1 x2 aa)
 5. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> pspace_aligned (?s51 ctea c a b x1 x2 aa)
 6. \<And>ctea c a b x1 x2 aa. \<lbrakk>cte_wp_at ((=) cap) p s; ctes_of s' (cte_map p) = Some (CTE x1 x2); invs s; valid_list s; invs' s'; cap \<noteq> cap.NullCap; x1 \<noteq> capability.NullCap; descendants_of p (cdt s) \<noteq> {}; cte_map aa \<noteq> nullPointer; ekheap_relation (ekheap s) (ksPSpace s'); ctes_of s' (cte_map aa) = Some ctea; isMDBParentOf (CTE x1 x2) ctea; 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'); revokable_relation (is_original_cap s) (null_filter (caps_of_state 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'; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap ctea); mdbNext x2 = cte_map aa; cte_map (a, b) = cte_map aa; cte = CTE x1 x2; next_child p (cdt_list s) = Some aa; cte_wp_at (\<lambda>_. True) aa s; valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> pspace_distinct (?s51 ctea c a b x1 x2 aa) proof (prove)
goal:
No subgoals!