theory Finalise_DR

lemma descendants_of_page:
  "\<lbrakk>valid_mdb s;page_table_at oid s\<rbrakk>\<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {}" apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def) apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits) apply (rule ccontr) apply (clarsimp simp:valid_mdb_def dest!:not_emptyI) apply (frule(1) cdl_cdt_parent_cte_at_lift) apply clarsimp apply (simp add:descendants_of_eqv cte_at_cases) apply (clarsimp simp:transform_cslot_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; typ_at (AArch APageTable) oid s\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_mdb s; kheap s oid = Some ko; (case ko of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_mdb s; kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_mdb s; kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); KHeap_D.descendants_of (oid, 0) (transform s) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 a b. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); (a, b) \<in> KHeap_D.descendants_of (oid, 0) (transform s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 a b. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); (a, b) \<in> KHeap_D.descendants_of (oid, 0) (transform s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<exists>slot. cte_wp_at (\<lambda>_. True) slot s \<and> (oid, 0) = transform_cslot_ptr slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 a b aa ba. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); (a, b) \<in> KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); cte_wp_at (\<lambda>_. True) (aa, ba) s; (oid, 0) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 a b aa ba. \<lbrakk>kheap s oid = Some (ArchObj (arch_kernel_obj.PageTable x2)); (a, b) \<in> transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); (\<exists>sz fun. kheap s aa = Some (kernel_object.CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> ba \<in> dom fun) \<or> (\<exists>tcb. kheap s aa = Some (TCB tcb)) \<and> ba \<in> dom tcb_cap_cases; (oid, 0) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!