theory CSpace1_R

lemma ensureNoChildren_corres:
  "p' = cte_map p \<Longrightarrow>
  corres (ser \<oplus> dc) (cte_at p) (pspace_aligned' and pspace_distinct' and cte_at' p' and valid_mdb')
         (ensure_no_children p) (ensureNoChildren p')" apply (simp add: ensureNoChildren_def ensure_no_children_descendants
                   liftE_bindE nullPointer_def) apply (rule corres_symb_exec_r) defer apply (rule getCTE_sp) apply wp apply (rule no_fail_pre, wp) apply simp apply (case_tac "mdbNext (cteMDBNode cte) = 0") apply (simp add: whenE_def) apply (clarsimp simp: returnOk_def corres_underlying_def return_def) apply (erule notE) apply (clarsimp simp: state_relation_def cdt_relation_def
                   simp del: split_paired_All) apply (erule allE, erule (1) impE) apply (subgoal_tac "descendants_of' (cte_map p) (ctes_of b) = {}") apply simp apply (clarsimp simp: descendants_of'_def) apply (subst (asm) cte_wp_at_ctes_of) apply clarsimp apply (erule (2) subtree_next_0) apply (simp add: whenE_def) apply (rule corres_symb_exec_r) defer apply (rule getCTE_sp) apply wp apply (rule no_fail_pre, wp) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) apply (erule (2) valid_dlistEn) apply simp apply clarsimp apply (rule conjI) apply (clarsimp simp: corres_underlying_def
                         throwError_def returnOk_def return_def) apply (subgoal_tac "pspace_aligned' b \<and> pspace_distinct' b") prefer 2 apply fastforce apply (clarsimp simp: cte_wp_at_ctes_of) apply (clarsimp simp: state_relation_def cdt_relation_def
                   simp del: split_paired_All) apply (erule allE, erule (1) impE) apply (clarsimp simp: descendants_of'_def) apply (subgoal_tac "ctes_of b \<turnstile> cte_map p \<rightarrow> mdbNext (cteMDBNode cte)") apply simp apply (rule direct_parent) apply (simp add: mdb_next_unfold) apply assumption apply (simp add: parentOf_def) apply clarsimp apply (clarsimp simp: corres_underlying_def
                        throwError_def returnOk_def return_def) apply (subgoal_tac "pspace_aligned' b \<and> pspace_distinct' b") prefer 2 apply fastforce apply (clarsimp simp: cte_wp_at_ctes_of) apply (clarsimp simp: state_relation_def cdt_relation_def
                  simp del: split_paired_All) apply (erule allE, erule (1) impE) apply (subgoal_tac "descendants_of' (cte_map p) (ctes_of b) = {}") apply simp apply (clarsimp simp: descendants_of'_def) apply (erule (4) subtree_no_parent) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) p' and valid_mdb') (ensure_no_children p) (ensureNoChildren p') proof (prove)
goal (1 subgoal):
 1. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (do cte <- getCTE (cte_map p);
whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)
od) proof (prove)
goal (4 subgoals):
 1. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (?Q'1 cte) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od))
 2. p' = cte_map p \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'\<rbrace> getCTE (cte_map p) \<lbrace>?Q'1\<rbrace>
 3. \<And>s. \<lbrakk>p' = cte_map p; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>p' = cte_map p; True\<rbrakk> \<Longrightarrow> no_fail (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') (getCTE (cte_map p)) proof (prove)
goal (4 subgoals):
 1. p' = cte_map p \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'\<rbrace> getCTE (cte_map p) \<lbrace>?Q'1\<rbrace>
 2. \<And>s. \<lbrakk>p' = cte_map p; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>p' = cte_map p; True\<rbrakk> \<Longrightarrow> no_fail (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') (getCTE (cte_map p))
 4. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (?Q'1 cte) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>p' = cte_map p; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map p) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>p' = cte_map p; True\<rbrakk> \<Longrightarrow> no_fail (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') (getCTE (cte_map p))
 3. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' = cte_map p; True\<rbrakk> \<Longrightarrow> no_fail (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') (getCTE (cte_map p))
 2. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p' = cte_map p; True; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb') s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map p) s
 2. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. p' = cte_map p \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od))
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ())
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (throwError ExceptionTypes_A.syscall_error.RevokeFirst a). case x of (r, t) \<Rightarrow> (t, b) \<in> state_relation \<and> r = Inr ()
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); \<forall>c. cte_wp_at (\<lambda>_. True) c a \<longrightarrow> cte_map ` descendants_of c (cdt a) = descendants_of' (cte_map c) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (3 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b); descendants_of' (cte_map p) (ctes_of b) = {}\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of' (cte_map p) (ctes_of b) = {}
 3. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of' (cte_map p) (ctes_of b) = {}
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b x. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = {c'. ctes_of b \<turnstile> cte_map p \<rightarrow> c'}; ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b x. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; \<exists>ctea. ctes_of b (cte_map p) = Some ctea \<and> ctea = cte; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = {c'. ctes_of b \<turnstile> cte_map p \<rightarrow> c'}; ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>cte a b x. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) = 0; cte_wp_at (\<lambda>_. True) p a; ctes_of b (cte_map p) = Some cte; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = {c'. ctes_of b \<turnstile> cte_map p \<rightarrow> c'}; ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (whenE (mdbNext (cteMDBNode cte) \<noteq> 0) (do next <- getCTE (mdbNext (cteMDBNode cte));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (do next <- getCTE (mdbNext (cteMDBNode cte));
if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()
od) proof (prove)
goal (4 subgoals):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (?Q'77 cte next) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ())
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')\<rbrace> getCTE (mdbNext (cteMDBNode cte)) \<lbrace>?Q'77 cte\<rbrace>
 3. \<And>cte s. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (mdbNext (cteMDBNode cte)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (getCTE (mdbNext (cteMDBNode cte))) proof (prove)
goal (4 subgoals):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')\<rbrace> getCTE (mdbNext (cteMDBNode cte)) \<lbrace>?Q'77 cte\<rbrace>
 2. \<And>cte s. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (mdbNext (cteMDBNode cte)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (getCTE (mdbNext (cteMDBNode cte)))
 4. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (?Q'77 cte next) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (3 subgoals):
 1. \<And>cte s. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (mdbNext (cteMDBNode cte)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (getCTE (mdbNext (cteMDBNode cte)))
 3. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) (getCTE (mdbNext (cteMDBNode cte)))
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte s. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; True; (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb')) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte s. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; pspace_aligned' s; pspace_distinct' s; ctes_of s (cte_map p) = Some 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> \<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte s cte'. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; pspace_aligned' s; pspace_distinct' s; ctes_of s (cte_map p) = Some cte; 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 p\<rbrakk> \<Longrightarrow> \<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (1 subgoal):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (if isMDBParentOf cte next then throwError Fault_H.syscall_error.RevokeFirst else returnOk ()) proof (prove)
goal (1 subgoal):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> (isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (throwError Fault_H.syscall_error.RevokeFirst)) \<and> (\<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ())) proof (prove)
goal (2 subgoals):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (throwError Fault_H.syscall_error.RevokeFirst)
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (3 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}\<rbrakk> \<Longrightarrow> pspace_aligned' b \<and> pspace_distinct' b
 3. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (3 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}\<rbrakk> \<Longrightarrow> pspace_aligned' b \<and> pspace_distinct' b
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> False
 3. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); \<forall>c. cte_wp_at (\<lambda>_. True) c a \<longrightarrow> cte_map ` descendants_of c (cdt a) = descendants_of' (cte_map c) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (3 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x; ctes_of b \<turnstile> cte_map p \<rightarrow> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p \<rightarrow> mdbNext (cteMDBNode cte)
 3. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p \<rightarrow> mdbNext (cteMDBNode cte)
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (4 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p \<leadsto> mdbNext (cteMDBNode cte)
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 3. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 4. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (3 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 3. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; descendants_of p (cdt a) = {}; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<not> ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> ctes_of b \<turnstile> cte_map p parentOf mdbNext (cteMDBNode cte)
 2. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (1 subgoal):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> isMDBParentOf cte next \<longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (1 subgoal):
 1. \<And>cte next. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (cte_wp_at (\<lambda>_. True) p) (cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) and (cte_wp_at' (\<lambda>c. c = cte) (cte_map p) and (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p) and valid_mdb'))) (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError ExceptionTypes_A.syscall_error.RevokeFirst s) (returnOk ()) proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b\<rbrakk> \<Longrightarrow> pspace_aligned' b \<and> pspace_distinct' b proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b\<rbrakk> \<Longrightarrow> pspace_aligned' b \<and> pspace_distinct' b
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; cte_wp_at' (\<lambda>c. c = next) (mdbNext (cteMDBNode cte)) b; cte_wp_at' (\<lambda>c. c = cte) (cte_map p) b; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; valid_mdb' b; pspace_aligned' b \<and> pspace_distinct' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; (a, b) \<in> state_relation; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); \<forall>c. cte_wp_at (\<lambda>_. True) c a \<longrightarrow> cte_map ` descendants_of c (cdt a) = descendants_of' (cte_map c) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {} proof (prove)
goal (2 subgoals):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b); descendants_of' (cte_map p) (ctes_of b) = {}\<rbrakk> \<Longrightarrow> descendants_of p (cdt a) = {}
 2. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of' (cte_map p) (ctes_of b) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = descendants_of' (cte_map p) (ctes_of b)\<rbrakk> \<Longrightarrow> descendants_of' (cte_map p) (ctes_of b) = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte next a b x. \<lbrakk>p' = cte_map p; mdbNext (cteMDBNode cte) \<noteq> 0; \<not> isMDBParentOf cte next; cte_wp_at (\<lambda>_. True) p a; ctes_of b (mdbNext (cteMDBNode cte)) = Some next; ctes_of b (cte_map p) = Some cte; valid_mdb' b; pspace_aligned' b; pspace_distinct' b; pspace_relation (kheap a) (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; cte_map ` descendants_of p (cdt a) = {c'. ctes_of b \<turnstile> cte_map p \<rightarrow> c'}; ctes_of b \<turnstile> cte_map p \<rightarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!