From 4c79675879e86e6eddbae6440f6b015a78f8ae1e Mon Sep 17 00:00:00 2001
From: Callum Bannister <callum.bannister@data61.csiro.au>
Date: Fri, 25 Jan 2019 16:38:20 +1100
Subject: [PATCH] sysinit: implement support for shared frames

Co-authored-by: Michael Sproul <michael.sproul@data61.csiro.au>
---
 proof/capDL-api/KHeap_DP.thy               |    1 -
 proof/sep-capDL/Helpers_SD.thy             |  140 +-
 spec/capDL/Types_D.thy                     |    2 +-
 sys-init/DuplicateCaps_SI.thy              |   82 +-
 sys-init/InitCSpace_SI.thy                 |    7 +-
 sys-init/InitTCB_SI.thy                    |    1 -
 sys-init/InitVSpace_SI.thy                 | 1916 ++++++++++----------
 sys-init/Mapped_Separating_Conjunction.thy |  216 +++
 sys-init/ObjectInitialised_SI.thy          |   33 +
 sys-init/Proof_SI.thy                      |  172 +-
 sys-init/RootTask_SI.thy                   |   69 +-
 sys-init/SysInit_SI.thy                    |  182 +-
 sys-init/WellFormed_SI.thy                 |  382 ++--
 13 files changed, 1950 insertions(+), 1253 deletions(-)
 create mode 100644 sys-init/Mapped_Separating_Conjunction.thy

diff --git a/proof/capDL-api/KHeap_DP.thy b/proof/capDL-api/KHeap_DP.thy
index ef5b28818..2f77c1317 100644
--- a/proof/capDL-api/KHeap_DP.thy
+++ b/proof/capDL-api/KHeap_DP.thy
@@ -545,7 +545,6 @@ lemma reset_cap_asid_cap_has_object:
 lemma cap_object_reset_cap_asid:
   "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_object cap = cap_object cap'"
   apply (case_tac cap',simp_all add:reset_cap_asid_def split:cdl_cap.split_asm)
-  apply (simp add:cap_object_def cap_has_object_def)+
   done
 
 lemma cap_type_reset_cap_asid[simp]:
diff --git a/proof/sep-capDL/Helpers_SD.thy b/proof/sep-capDL/Helpers_SD.thy
index de0e86ed1..822a19eef 100644
--- a/proof/sep-capDL/Helpers_SD.thy
+++ b/proof/sep-capDL/Helpers_SD.thy
@@ -455,6 +455,12 @@ lemma object_size_bits_empty_cnode [simp]:
   "object_size_bits (CNode (empty_cnode sz)) = sz"
   by (clarsimp simp: object_size_bits_def empty_cnode_def)
 
+lemma is_pt_pt_size[simp]: "is_pt obj \<Longrightarrow> object_size_bits obj = pt_size"
+  by (clarsimp simp: object_size_bits_def pt_size_def is_pt_def split: cdl_object.splits)
+
+lemma is_pd_pd_size[simp]: "is_pd obj \<Longrightarrow> object_size_bits obj = pd_size"
+  by (clarsimp simp: object_size_bits_def pt_size_def is_pd_def split: cdl_object.splits)
+
 definition
   object_at_pointer_size_bits :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_size_bits"
 where
@@ -550,7 +556,7 @@ definition
   "real_object_at \<equiv> \<lambda> obj_id s. obj_id \<in> dom (cdl_objects s) \<and> obj_id \<notin> irq_nodes s"
 
 
-(* Agregate object types. *)
+(* Aggregate object types. *)
 abbreviation
   "table_at \<equiv> \<lambda>obj_id s. pt_at obj_id s \<or> pd_at obj_id s"
 abbreviation
@@ -609,6 +615,9 @@ lemma object_type_is_object:
                     is_cnode_def is_irq_node_def is_asidpool_def is_pt_def is_pd_def is_frame_def
              split: cdl_object.splits)
 
+lemma is_ptD[dest]: "is_pt obj \<Longrightarrow> \<exists>x. obj = PageTable x"
+  by (clarsimp simp: is_pt_def split: cdl_object.splits)
+
 lemma object_at_object_type:
   "\<lbrakk>cdl_objects spec obj_id = Some obj; untyped_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = UntypedType"
   "\<lbrakk>cdl_objects spec obj_id = Some obj; ep_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = EndpointType"
@@ -619,6 +628,7 @@ lemma object_at_object_type:
   "\<lbrakk>cdl_objects spec obj_id = Some obj; asidpool_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = AsidPoolType"
   "\<lbrakk>cdl_objects spec obj_id = Some obj; pt_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageTableType"
   "\<lbrakk>cdl_objects spec obj_id = Some obj; pd_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageDirectoryType"
+  "\<lbrakk>cdl_objects spec obj_id = Some obj; frame_at obj_id spec\<rbrakk> \<Longrightarrow> \<exists>n. object_type obj = FrameType n"
   by (simp_all add: object_at_def object_type_is_object)
 
 lemma object_type_object_at:
@@ -642,6 +652,15 @@ lemma set_object_type [simp]:
   "{obj_id \<in> dom (cdl_objects spec). real_object_at obj_id spec} = {obj_id. real_object_at obj_id spec}"
   by (auto simp: object_at_def real_object_at_def)
 
+lemma pt_at_is_real[simp]: "pt_at pt_id spec \<Longrightarrow> pt_id \<in> {obj_id. real_object_at obj_id spec}"
+  apply (clarsimp simp: object_at_def is_pt_def real_object_at_def dom_def
+                        irq_nodes_def is_irq_node_def)
+  by (clarsimp split: cdl_object.splits)
+
+lemma pd_at_is_real[simp]: "pd_at pt_id spec \<Longrightarrow> pt_id \<in> {obj_id. real_object_at obj_id spec}"
+  apply (clarsimp simp: object_at_def is_pd_def real_object_at_def dom_def
+                        irq_nodes_def is_irq_node_def)
+  by (clarsimp split: cdl_object.splits)
 
 definition
   real_objects :: "cdl_state \<Rightarrow> cdl_object_id set"
@@ -666,6 +685,34 @@ where "is_fake_pt_cap cap \<equiv> case cap of
     PageTableCap _ Fake _ \<Rightarrow> True
   | _ \<Rightarrow> False"
 
+definition is_real_vm_cap :: "cdl_cap \<Rightarrow> bool"
+where
+  "is_real_vm_cap cap \<equiv>
+       (case cap of
+           FrameCap _ _ _ _ Real _     \<Rightarrow> True
+         | PageTableCap _ Real _     \<Rightarrow> True
+         | PageDirectoryCap _ Real _ \<Rightarrow> True
+         | _                         \<Rightarrow> False)"
+
+definition is_fake_vm_cap :: "cdl_cap \<Rightarrow> bool"
+where
+  "is_fake_vm_cap cap \<equiv>
+       (case cap of
+           FrameCap _ _ _ _ Fake _     \<Rightarrow> True
+         | PageTableCap _ Fake _     \<Rightarrow> True
+         | PageDirectoryCap _ Fake _ \<Rightarrow> True
+         | _                         \<Rightarrow> False)"
+
+abbreviation
+  "fake_frame_cap dev ptr rights n \<equiv> FrameCap dev ptr rights n Fake None"
+abbreviation
+  "is_fake_frame_cap cap \<equiv> (case cap of FrameCap _ _ _ _ Fake None \<Rightarrow> True | _ \<Rightarrow> False)"
+
+definition dev_of :: "cdl_cap \<Rightarrow> bool option" where
+  "dev_of cap = (case cap of FrameCap dev ptr _ n _ _ \<Rightarrow> Some dev | _ \<Rightarrow> None)"
+definition cap_size_bits :: "cdl_cap \<Rightarrow> nat" where
+  "cap_size_bits cap = (case cap of FrameCap _ _ _ n _ _ \<Rightarrow> n | _ \<Rightarrow> 0)"
+
 lemma is_fake_pt_cap_is_pt_cap [elim!]:
   "is_fake_pt_cap cap \<Longrightarrow> is_pt_cap cap"
   by (clarsimp simp: is_fake_pt_cap_def split: cdl_cap.splits)
@@ -824,6 +871,24 @@ lemma cap_object_default_cap_frame:
   "is_frame_cap cap \<Longrightarrow> cap_object (default_cap (the (cap_type cap)) {obj_id} sz dev) = obj_id"
   by clarsimp
 
+lemma is_pd_default_cap[simp]:
+  "is_pd obj \<Longrightarrow>
+   cdl_objects spec ptr = Some obj \<Longrightarrow>
+   default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None"
+  by (clarsimp simp: object_type_is_object default_cap_def)
+
+lemma pd_at_default_cap[simp]:
+  "pd_at ptr spec \<Longrightarrow>
+   cdl_objects spec ptr = Some obj \<Longrightarrow>
+   default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None"
+  by (fastforce simp: object_at_def)
+
+lemma pt_at_default_cap[simp]:
+  "pt_at ptr spec \<Longrightarrow>
+   cdl_objects spec ptr = Some obj \<Longrightarrow>
+   default_cap (object_type obj) {ptr'} n b = PageTableCap ptr' Real None"
+  by (clarsimp simp: object_type_is_object default_cap_def object_at_def)
+
 lemma default_cap_not_null [elim!]:
   "default_cap type obj_ids sz dev = NullCap \<Longrightarrow> False"
   "NullCap = default_cap type obj_ids sz dev\<Longrightarrow> False"
@@ -835,7 +900,7 @@ lemma cap_objects_update_cap_object [simp]:
   by (clarsimp simp: cap_has_object_def update_cap_object_def
               split: cdl_cap.splits)
 
-lemma  cap_has_object_default_cap [simp]:
+lemma cap_has_object_default_cap [simp]:
   "type \<noteq> IRQNodeType \<Longrightarrow> cap_has_object (default_cap type ids sz dev)"
   by (clarsimp simp: default_cap_def cap_has_object_def split: cdl_object_type.splits)
 
@@ -1124,4 +1189,75 @@ lemma inter_empty_not_both:
 "\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B"
   by fastforce
 
+lemma object_at_predicate_lift:
+  "object_at P obj_id spec \<Longrightarrow> P (the (cdl_objects spec obj_id))"
+  by (fastforce simp: object_at_def)
+
+lemma object_at_cdl_objects_elim[elim]:
+  "object_at P obj_id spec \<Longrightarrow> cdl_objects spec obj_id = Some (the (cdl_objects spec obj_id))"
+  by (fastforce simp: object_at_def)
+
+lemma opt_cap_object_slot:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   P (object_slots obj slot) \<Longrightarrow>
+   P (opt_cap (obj_id, slot) spec)"
+  by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
+
+lemma opt_cap_object_slotE:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   object_slots obj slot = Some cap \<Longrightarrow>
+   opt_cap (obj_id, slot) spec = Some cap"
+  by (rule opt_cap_object_slot)
+
+lemma slots_of_object_slot:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   P (object_slots obj slot) \<Longrightarrow>
+   P (slots_of obj_id spec slot)"
+   by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
+
+lemma slots_of_object_slotE:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   object_slots obj slot = Some cap \<Longrightarrow>
+   slots_of obj_id spec slot = Some cap"
+   by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
+
+lemma object_at_cdl_objects:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   P obj \<Longrightarrow>
+   object_at P obj_id spec"
+  by (fastforce simp: object_at_def)
+
+lemma opt_cap_object_slot_simp:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   opt_cap (obj_id, slot) spec = object_slots obj slot"
+   by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
+
+lemma slots_of_object_slot_simp:
+  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
+   slots_of obj_id spec slot = object_slots obj slot"
+   by (fastforce simp: object_at_def opt_cap_def slots_of_def opt_object_def)
+
+lemma is_fake_pt_cap_cap_has_object:
+  "is_fake_pt_cap cap \<Longrightarrow> cap_has_object cap"
+  by (clarsimp simp: cap_has_object_def is_fake_pt_cap_def split: cdl_cap.splits)
+
+lemma is_fake_pt_cap_pt_cap:
+  "is_fake_pt_cap (PageTableCap x R z) \<longleftrightarrow> R = Fake"
+  by (clarsimp simp: is_fake_pt_cap_def split: cdl_frame_cap_type.splits)
+
+lemma fake_vm_cap_simp:
+  "is_fake_vm_cap (FrameCap x y z a R b) \<longleftrightarrow> R = Fake"
+  by (clarsimp simp: is_fake_vm_cap_def split: cdl_frame_cap_type.splits)
+
+lemma frame_not_pt[intro!]: "\<not> (is_frame x \<and> is_pt x)"
+  by (cases x; clarsimp simp: is_frame_def is_pt_def)
+
+lemma not_frame_and_pt: "is_frame x \<Longrightarrow> is_pt x \<Longrightarrow> False"
+  by (fastforce simp: frame_not_pt[simplified])
+
+lemma not_cap_at_cap_not_at:
+  "(slot \<in> dom (slots_of obj_id spec) \<and> \<not> cap_at P (obj_id, slot) spec) \<longleftrightarrow>
+   (slot \<in> dom (slots_of obj_id spec) \<and> cap_at (\<lambda>x. \<not> P x) (obj_id, slot) spec)"
+  by (intro iffI; clarsimp simp: cap_at_def opt_cap_def)
+
 end
diff --git a/spec/capDL/Types_D.thy b/spec/capDL/Types_D.thy
index 5be7440a3..18752a717 100644
--- a/spec/capDL/Types_D.thy
+++ b/spec/capDL/Types_D.thy
@@ -354,7 +354,7 @@ where
      then (THE c. c \<in> cap_objects cap)
      else undefined"
 
-lemma cap_object_simps:
+lemma cap_object_simps[simp]:
   "cap_object (IOPageTableCap x) = x"
   "cap_object (IOSpaceCap x) = x"
   "cap_object (IOPortsCap x a) = x"
diff --git a/sys-init/DuplicateCaps_SI.thy b/sys-init/DuplicateCaps_SI.thy
index 866dcf81c..91674d6fd 100644
--- a/sys-init/DuplicateCaps_SI.thy
+++ b/sys-init/DuplicateCaps_SI.thy
@@ -31,11 +31,6 @@ lemma sep_map_zip_snd_take:
   apply simp
   done
 
-lemma sep_map_c_unat [simp]:
-  "(\<lambda>slot. (obj_id, slot) \<mapsto>c NullCap) \<circ> unat =
-   (\<lambda>cptr. (obj_id, unat cptr) \<mapsto>c NullCap)"
-  by fastforce
-
 lemma wfdc_obj_not_untyped:
   "well_formed_cap (default_cap t oid sz dev) \<Longrightarrow> t \<noteq> UntypedType"
   by (clarsimp simp:default_cap_def well_formed_cap_def)
@@ -48,13 +43,21 @@ lemma derived_cap_default:
 
 lemma cnode_or_tcb_at_wfc:
   "\<lbrakk>cnode_or_tcb_at obj_id spec; cdl_objects spec obj_id = Some obj; sz \<le> 32\<rbrakk>
-  \<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
+   \<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
   apply (elim disjE)
    apply (simp add: object_at_def is_tcb_def default_cap_def well_formed_cap_def
                     is_cnode_def object_type_def guard_bits_def
              split: cdl_object.splits)+
   done
 
+lemma frame_at_wfc:
+  "\<lbrakk>frame_at obj_id spec; cdl_objects spec obj_id = Some obj; sz \<le> 32\<rbrakk>
+   \<Longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev)"
+   apply (simp add: object_at_def is_frame_def default_cap_def well_formed_cap_def
+                    is_cnode_def object_type_def guard_bits_def vm_read_write_def
+             split: cdl_object.splits)
+  done
+
 lemma seL4_CNode_Copy_sep_helper:
   "\<lbrakk>(free_cptr::32 word) < 2 ^ si_cnode_size;
     (cap_ptr::32 word) < 2 ^ si_cnode_size;
@@ -96,17 +99,54 @@ lemma seL4_CNode_Copy_sep_helper:
   apply sep_solve
   done
 
-lemma duplicate_cap_sep_helper:
+(* This definition is a bit of a hack for the duplicate_cap_sep_helper_general lemma below.
+   Originally it only supported CNodes and TCBs, but it has been extended with support for'
+   duplicating frames *)
+definition well_formed_obj_filter ::
+  "(cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> bool) \<Rightarrow> bool"
+  where
+  "well_formed_obj_filter obj_filter \<equiv>
+     \<forall>spec obj_id obj.
+        obj_filter obj_id spec \<and> cdl_objects spec obj_id = Some obj
+        \<longrightarrow> (\<forall>oid sz dev. sz \<le> 32 \<longrightarrow> well_formed_cap (default_cap (object_type obj) oid sz dev))
+            \<and> (well_formed spec \<longrightarrow> real_object_at obj_id spec)"
+
+lemma wf_obj_filter_wfc:
+  "\<lbrakk>well_formed_obj_filter obj_filter;
+    obj_filter obj_id spec;
+    cdl_objects spec obj_id = Some obj;
+    sz \<le> 32\<rbrakk> \<Longrightarrow>
+   well_formed_cap (default_cap (object_type obj) oid sz dev)"
+  by (clarsimp simp: well_formed_obj_filter_def)
+
+lemma wf_obj_filter_real_object_at:
+  "\<lbrakk>well_formed_obj_filter obj_filter;
+    well_formed spec;
+    obj_filter obj_id spec;
+    cdl_objects spec obj_id = Some obj\<rbrakk> \<Longrightarrow>
+   real_object_at obj_id spec"
+  by (clarsimp simp: well_formed_obj_filter_def)
+
+lemma wf_obj_filter_cnode_or_tcb_at:
+  "well_formed_obj_filter cnode_or_tcb_at"
+  by (auto simp: well_formed_obj_filter_def object_at_real_object_at intro: cnode_or_tcb_at_wfc)
+
+lemma wf_obj_filter_frame_at:
+  "well_formed_obj_filter frame_at"
+  by (auto simp: well_formed_obj_filter_def object_at_real_object_at intro: frame_at_wfc)
+
+lemma duplicate_cap_sep_helper_general:
   "\<lbrakk>well_formed spec; distinct obj_ids;
    list_all (\<lambda>n. n < 2 ^ si_cnode_size) (map unat free_cptrs);
-   (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs);
+   well_formed_obj_filter obj_filter;
+   (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs);
     set obj_ids = dom (cdl_objects spec)\<rbrakk>
   \<Longrightarrow>
   \<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
      si_cap_at t orig_caps spec dev obj_id \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>
     duplicate_cap spec orig_caps (obj_id, free_cptr)
   \<lbrace>\<lambda>_ s.
-   \<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs))
+   \<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs))
                 spec dev obj_id \<and>*
     si_cap_at t orig_caps spec dev obj_id \<and>* si_objects \<and>* R\<guillemotright> s\<rbrace>"
   apply (rule hoare_assume_pre)
@@ -126,26 +166,27 @@ lemma duplicate_cap_sep_helper:
               seL4_CNode_Copy_sep_helper)
         apply (rule unat_less_2_si_cnode_size, simp)
        apply simp
-      apply (erule(1) cnode_or_tcb_at_wfc)
-       apply (frule (1) well_formed_object_size_bits_word_bits, simp add: word_bits_def)
-      apply sep_solve
+      apply (erule (2) wf_obj_filter_wfc)
+      apply (frule (1) well_formed_object_size_bits_word_bits, simp add: word_bits_def)
      apply sep_solve
+    apply sep_solve
    apply (rule conjI)
     apply (rule unat_less_2_si_cnode_size, simp)
    apply sep_solve
   apply clarsimp
   done
 
-lemma duplicate_cap_sep:
+lemma duplicate_cap_sep_general:
   "\<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R\<guillemotright> and K (
     well_formed spec \<and> distinct obj_ids \<and>
     list_all (\<lambda>n. n < 2 ^ si_cnode_size) (map unat free_cptrs) \<and>
-    (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs) \<and>
+    well_formed_obj_filter obj_filter \<and>
+    (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs) \<and>
     set obj_ids = dom (cdl_objects spec))\<rbrace>
       duplicate_cap spec orig_caps (obj_id, free_cptr)
   \<lbrace>\<lambda>_.
-   \<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs))
+   \<guillemotleft>si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec] free_cptrs))
                 spec dev obj_id \<and>*
     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R\<guillemotright>\<rbrace>"
   apply (rule hoare_gen_asm)
@@ -155,15 +196,14 @@ lemma duplicate_cap_sep:
   apply (rule hoare_chain [where
    P="\<guillemotleft>((si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>* si_objects) \<and>*
         (\<And>* obj_id \<in> {obj_id. real_object_at obj_id spec}. si_cap_at t orig_caps spec dev obj_id) \<and>* R\<guillemotright>" and
-   Q="\<lambda>rv.\<guillemotleft>(si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec]
+   Q="\<lambda>rv.\<guillemotleft>(si_cap_at t (map_of (zip [obj\<leftarrow>obj_ids. obj_filter obj spec]
             free_cptrs)) spec dev obj_id \<and>* si_objects) \<and>*
         (\<And>* obj_id \<in> {obj_id. real_object_at obj_id spec}. si_cap_at t orig_caps spec dev obj_id) \<and>* R\<guillemotright>"])
     apply (rule sep_set_conj_map_singleton_wp [where x=obj_id])
       apply simp
-     apply (drule in_set_zip1)
-     apply (fastforce simp: object_at_real_object_at)
+     apply (fastforce dest: in_set_zip1 simp: wf_obj_filter_real_object_at)
     apply (rule hoare_chain)
-      apply (rule_tac t=t and R=R in duplicate_cap_sep_helper, assumption+)
+      apply (rule_tac t=t and R=R in duplicate_cap_sep_helper_general, fastforce+)
      apply sep_solve
     apply sep_solve
    apply sep_solve
@@ -171,6 +211,8 @@ lemma duplicate_cap_sep:
   apply sep_solve
   done
 
+lemmas duplicate_cap_sep = duplicate_cap_sep_general[where obj_filter=cnode_or_tcb_at]
+
 lemma duplicate_caps_sep_helper:
   "\<lbrace>\<guillemotleft>si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
      (\<And>* (obj_id, free_cptr) \<in> set (zip [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] free_cptrs).
@@ -201,7 +243,7 @@ lemma duplicate_caps_sep_helper:
      apply (clarsimp simp: sep_conj_assoc)
      apply (rename_tac obj_id free_cptr)
      apply (wp sep_wp: duplicate_cap_sep [where obj_ids=obj_ids and free_cptrs=free_cptrs and t=t])
-     apply clarsimp
+     apply (clarsimp simp: wf_obj_filter_cnode_or_tcb_at)
      apply sep_solve
     apply (clarsimp simp: sep_conj_assoc si_caps_at_def)
     apply sep_solve
diff --git a/sys-init/InitCSpace_SI.thy b/sys-init/InitCSpace_SI.thy
index 2a38fb700..3f2968084 100644
--- a/sys-init/InitCSpace_SI.thy
+++ b/sys-init/InitCSpace_SI.thy
@@ -14,6 +14,7 @@ imports
   ObjectInitialised_SI
   RootTask_SI
   SysInit_SI
+  Mapped_Separating_Conjunction
 begin
 
 (****************************
@@ -1740,10 +1741,6 @@ lemma set_take_add:
    set (take i zs) \<union> set (take j (drop i zs)) = set (take k zs)"
   by (metis set_append take_add)
 
-lemma sep_map_set_conj_set_cong:
-  "\<lbrakk>sep_map_set_conj f xs s; xs = ys\<rbrakk> \<Longrightarrow> sep_map_set_conj f ys s"
-  by simp
-
 lemma wellformed_no_dev:
   "well_formed spec \<Longrightarrow>(\<forall>obj_id. cnode_at obj_id spec \<longrightarrow>
                        (\<forall>slot\<in>dom (slots_of obj_id spec). cap_at (\<lambda>c. is_device_cap c = False) (obj_id, slot) spec))"
@@ -1800,7 +1797,7 @@ lemma init_cspace_sep:
                    and irqs="used_irq_list spec"], simp+)
   apply (subst (asm) sep.prod.union_disjoint [symmetric], simp+)
    apply (metis (no_types) distinct_append distinct_take_strg inf_sup_aci(1) take_add)
-  apply (erule sep_map_set_conj_set_cong)
+  apply (erule sep_map_set_conj_set_cong[THEN fun_cong, THEN iffD1, rotated])
   apply clarsimp
   apply (subst Un_commute, subst set_take_add, (simp add: add.commute)+)
   done
diff --git a/sys-init/InitTCB_SI.thy b/sys-init/InitTCB_SI.thy
index f02761961..791123643 100644
--- a/sys-init/InitTCB_SI.thy
+++ b/sys-init/InitTCB_SI.thy
@@ -432,7 +432,6 @@ lemma tcb_configure_post:
   apply (clarsimp simp: si_objects_def)
   apply (clarsimp simp: sep_conj_exists sep_conj_assoc)
   apply (clarsimp simp: si_cap_at_def sep_conj_assoc sep_conj_exists)
-  apply (clarsimp simp: object_at_def)
   apply (subst tcb_half_decomp' [where obj_id=obj_id and k_obj_id=k_obj_id],
          (assumption|simp)+)
   apply (subst (asm) sep_map_f_eq_tcb_fault_endpoint, assumption+)
diff --git a/sys-init/InitVSpace_SI.thy b/sys-init/InitVSpace_SI.thy
index f51f3e2aa..77dcb4398 100644
--- a/sys-init/InitVSpace_SI.thy
+++ b/sys-init/InitVSpace_SI.thy
@@ -16,105 +16,124 @@ imports
   ObjectInitialised_SI
   RootTask_SI
   SysInit_SI
+  DuplicateCaps_SI
+  "../lib/sep_algebra/Sep_Fold_Cancel"
+  "../lib/sep_algebra/Sep_Util"
+  "HOL-Library.Multiset"
+  Mapped_Separating_Conjunction
+  AInvs.Rights_AI
+  "../lib/Guess_ExI"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-lemma all_fake_pd_caps_in_pd:
-  "well_formed spec \<Longrightarrow>
-   {(obj_id, slot). pd_at obj_id spec \<and> fake_pt_cap_at (obj_id, slot) spec} =
-   {cap_ref. fake_pt_cap_at cap_ref spec}"
-   apply rule
-    apply clarsimp
-   apply (clarsimp simp: cap_at_def opt_cap_def)
-   apply (erule (2) well_formed_fake_pt_cap_in_pd)
-   done
+declare
+  object_at_predicate_lift[simp]
+  opt_cap_object_slot[simp]
+  opt_cap_object_slotE[elim]
+  slots_of_object_slot[simp]
+  slots_of_object_slotE[elim]
+  object_at_cdl_objects[simp]
 
-lemma is_fake_pt_cap_cap_has_object [simp]:
-  "is_fake_pt_cap cap \<Longrightarrow> cap_has_object cap"
-  by (clarsimp simp: cap_has_object_def is_fake_pt_cap_def split: cdl_cap.splits)
+(* Abbreviations for commonly appearing expressions involving virtual addresses and slots *)
+(* TODO: use pd_size, pt_size, small_frame_size instead of magic numbers *)
+abbreviation
+  "pd_slot_of_pt_vaddr vaddr \<equiv> vaddr >> 20 :: machine_word"
+abbreviation
+  "pt_slot_of_vaddr vaddr \<equiv> (vaddr >> 12) && 0xFF :: machine_word"
+abbreviation
+  "pt_vaddr_of_pd_slot pd_slot \<equiv> of_nat pd_slot << 20 :: machine_word"
+abbreviation
+  "frame_vaddr_of_slots pd_slot pt_slot \<equiv>
+    pt_vaddr_of_pd_slot pd_slot + (of_nat pt_slot << small_frame_size) :: machine_word"
 
-lemma is_fake_vm_cap_cap_has_object [simp]:
-  "is_fake_vm_cap cap \<Longrightarrow> cap_has_object cap"
-  by (clarsimp simp: cap_has_object_def is_fake_vm_cap_def split: cdl_cap.splits)
+(* FIXME: MOVE (Lib) *)
+lemma singleton_eq[simp]: "(\<lambda>v. if v = x then Some y else None) = [x \<mapsto> y]"
+  by (clarsimp simp: fun_upd_def)
 
-lemma cap_has_object_simps [simp]:
-  "cap_has_object (EndpointCap obj_id badge rights)"
-  "cap_has_object (NotificationCap obj_id badge rights)"
-  "cap_has_object (ReplyCap obj_id rights)"
-  "cap_has_object (MasterReplyCap obj_id)"
-  "cap_has_object (CNodeCap obj_id guard gs sz)"
-  "cap_has_object (TcbCap obj_id)"
-  "cap_has_object (PendingSyncSendCap obj_id badge a b c grant)"
-  "cap_has_object (PendingSyncRecvCap obj_id d grant)"
-  "cap_has_object (PendingNtfnRecvCap obj_id)"
-  "cap_has_object (FrameCap dev obj_id rights sz type maddr)"
-  "cap_has_object (PageTableCap obj_id cdl_frame_cap_type maddr)"
-  "cap_has_object (PageDirectoryCap obj_id cdl_frame_cap_type asid)"
-  "cap_has_object (AsidPoolCap obj_id as)"
-  "cap_has_object (IOPortsCap obj_id io)"
-  "cap_has_object (IOSpaceCap obj_id)"
-  "cap_has_object (IOPageTableCap obj_id)"
-  "cap_has_object (ZombieCap obj_id)"
-  by (clarsimp simp: cap_has_object_def)+
+lemma map_add_simp [simp]: "(\<lambda>p. if p = p' then Some v else f p) = f ++ [p' \<mapsto> v] "
+  by (intro ext iffI; clarsimp simp: map_add_def split: option.splits)
 
-lemma fake_pt_cap_at_conversion:
-  "well_formed spec
-  \<Longrightarrow> (\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}.
-       \<And>* slot\<in>set (slots_of_list spec obj_id).
-        if fake_pt_cap_at (obj_id, slot) spec then f (cap_ref_object (obj_id, slot) spec) else \<box>) =
-      (\<And>* obj_id \<in> {obj_id. \<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and> obj_id = cap_object cap}.
-           f obj_id)"
-  apply (subst sep.prod.Sigma, clarsimp+)
-  apply (subst sep_map_set_conj_restrict_predicate)
-   apply (rule finite_SigmaI, clarsimp+)
-  apply (subst fake_cap_rewrite, assumption)
-  apply (frule well_formed_pt_cap_bij)
-  apply (clarsimp simp: bij_betw_def)
-  apply (rule sep_map_set_conj_reindex_cong [where f="\<lambda>cap_ref. cap_ref_object cap_ref spec", symmetric])
-    apply (subst (asm) all_fake_pd_caps_in_pd, simp+)
-   apply (fastforce simp: image_def cap_ref_object_def cap_at_def all_caps_def)
-  apply (clarsimp)
-  done
+lemma list_all_spec: "list_all P xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> P x"
+  by (simp add: list_all_iff)
+(* /MOVE *)
 
 lemma empty_cap_map_shiftr_NullCap:
-  "empty_cap_map 12 (unat ((vaddr::word32) >> 20)) = Some NullCap"
+  "empty_cap_map 12 (unat ((vaddr :: word32) >> 20)) = Some NullCap"
   apply (clarsimp simp:empty_cap_map_def)
   apply (rule unat_less_helper)
   apply simp
-  apply (subst word32_less_sub_le[where n= 12,simplified,symmetric])
-   apply (simp add:word_bits_def)
-  apply (simp add: shiftr_shiftr
-    le_mask_iff[where n = 12,unfolded mask_def,simplified])
+  apply (subst word32_less_sub_le[where n=12, simplified, symmetric])
+   apply (simp add: word_bits_def)
+  apply (simp add: shiftr_shiftr le_mask_iff[where n=12, unfolded mask_def, simplified])
   apply (rule shiftr_eq_0)
   apply simp
   done
 
 lemma object_slot_initialised_lookup:
   "\<lbrakk>t spec_ptr = Some ptr; opt_cap (spec_ptr,slot) spec = Some cap\<rbrakk>
-  \<Longrightarrow> object_slot_initialised spec t spec_ptr slot = ((ptr,slot)\<mapsto>c (cap_transform t cap))"
-  apply (clarsimp simp:object_slot_initialised_def opt_object_def
-    object_initialised_general_def opt_cap_def slots_of_def
-    split:option.splits)
+   \<Longrightarrow> object_slot_initialised spec t spec_ptr slot = (ptr, slot) \<mapsto>c cap_transform t cap"
+  apply (clarsimp simp: object_slot_initialised_def opt_object_def
+                        object_initialised_general_def opt_cap_def slots_of_def
+                 split: option.splits)
   apply (intro ext iffI)
    apply (drule sep_map_c_sep_map_s[where cap = "cap_transform t cap"])
-    apply (simp add:spec2s_def update_slots_def object_slots_def
-      split:cdl_object.splits)
+    apply (simp add: spec2s_def update_slots_def object_slots_def split: cdl_object.splits)
    apply simp
   apply (subst (asm) sep_map_c_def2)
-  apply (clarsimp simp:spec2s_def)
-  apply (clarsimp simp:sep_map_s_def
-    sep_map_general_def object_to_sep_state_def)
+  apply (clarsimp simp: spec2s_def sep_map_s_def sep_map_general_def object_to_sep_state_def)
   apply (rule ext)
-  apply (clarsimp simp:object_project_def
-    object_slots_object_clean)
-  apply (clarsimp simp:update_slots_def
-    object_slots_def split:cdl_object.splits)
+  apply (clarsimp simp: object_project_def object_slots_object_clean)
+  apply (clarsimp simp: update_slots_def object_slots_def split: cdl_object.splits)
   done
 
-(*****************************
- * Mapping page directories. *
- *****************************)
+lemma seL4_Page_Map_object_initialised_sep:
+  "\<lbrace>\<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
+    object_slot_empty spec t (cap_object pt_cap) (unat (pt_slot_of_vaddr vaddr)) \<and>*
+    (si_cnode_id , offset sel4_page si_cnode_size) \<mapsto>c
+      FrameCap dev page_ptr vm_read_write n Real None \<and>*
+    (si_cnode_id , offset sel4_pd si_cnode_size) \<mapsto>c (PageDirectoryCap pd_ptr Real None) \<and>*
+    si_objects \<and>* R\<guillemotright> and
+  K(pd_at spec_pd_ptr spec \<and>
+    opt_cap (spec_pd_ptr, unat (vaddr >> 20)) spec = Some pt_cap \<and>
+    pt_cap = PageTableCap spec_pt_ptr Fake None \<and>
+    opt_cap (spec_pt_ptr, unat (pt_slot_of_vaddr vaddr)) spec
+      = Some (FrameCap False spec_page_ptr (validate_vm_rights rights) n Fake None) \<and>
+    cdl_objects spec (cap_object pt_cap) = Some cap_obj \<and>
+    sel4_page < 2 ^ si_cnode_size \<and>
+    vaddr = frame_vaddr_of_slots (unat (pd_slot_of_pt_vaddr vaddr))
+                                 (unat (pt_slot_of_vaddr vaddr)) \<and>
+    sel4_pd < 2 ^ si_cnode_size \<and>
+    object_slots (object_default_state cap_obj) (unat (pt_slot_of_vaddr vaddr)) = Some cap_slots \<and>
+    (n = 12 \<or> n = 16) \<and>
+    t (cap_object pt_cap) = Some pt_ptr \<and>
+    t spec_pd_ptr = Some pd_ptr \<and>
+    t spec_page_ptr = Some page_ptr)\<rbrace>
+     seL4_Page_Map sel4_page sel4_pd vaddr rights vmattribs
+   \<lbrace>\<lambda>rv. \<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
+   object_slot_initialised spec t (cap_object pt_cap) (unat (pt_slot_of_vaddr vaddr)) \<and>*
+   (si_cnode_id , offset sel4_page si_cnode_size) \<mapsto>c
+      FrameCap dev page_ptr vm_read_write n Real None \<and>*
+   (si_cnode_id , offset sel4_pd si_cnode_size) \<mapsto>c (PageDirectoryCap pd_ptr Real None) \<and>*
+   si_objects \<and>* R\<guillemotright>\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (wp sep_wp: seL4_Page_Map_wp[where n=n and cnode_cap= si_cspace_cap and
+                                           root_size = si_cnode_size and pt_ptr = pt_ptr])
+          apply fastforce+
+     apply (simp add: word_bits_def guard_equal_si_cspace_cap)+
+  apply clarsimp
+  apply sep_cancel+
+  apply (clarsimp simp: si_objects_def sep_conj_assoc sep_state_projection2_def root_tcb_def
+                        update_slots_def)
+  apply sep_cancel+
+  apply (clarsimp simp: object_slot_empty_def object_fields_empty_def
+                        object_initialised_general_def si_objects_def cdl_lookup_pd_slot_def
+                        root_tcb_def update_slots_def validate_vm_rights_inter_rw)
+  apply (sep_drule sep_map_c_sep_map_s)
+   apply (clarsimp, fastforce)
+  apply (clarsimp simp: object_slot_initialised_lookup shiftr_less cap_object_def)
+  apply sep_solve
+  done
 
 lemma seL4_PageTable_Map_object_initialised_sep:
   "\<lbrace>\<guillemotleft>object_slot_empty spec t pd_id (unat (shiftr vaddr 20)) \<and>*
@@ -125,11 +144,9 @@ lemma seL4_PageTable_Map_object_initialised_sep:
     pd_at pd_id spec \<and>
     opt_cap (pd_id, unat (shiftr vaddr 20)) spec = Some (PageTableCap pt_id Fake None) \<and>
 
-    (* Some word assumption *)
     sel4_pt < 2 ^ si_cnode_size \<and>
     sel4_pd < 2 ^ si_cnode_size \<and>
 
-    (* Following are some assumptions about t *)
     t pd_id = Some pd_ptr \<and>
     t pt_id = Some pt_ptr)\<rbrace>
      seL4_PageTable_Map sel4_pt sel4_pd vaddr vmattribs
@@ -138,82 +155,23 @@ lemma seL4_PageTable_Map_object_initialised_sep:
    (si_cnode_id, offset sel4_pd si_cnode_size) \<mapsto>c (PageDirectoryCap pd_ptr Real None) \<and>*
     si_objects \<and>* R\<guillemotright>\<rbrace>"
   apply (rule hoare_gen_asm)
-  apply (clarsimp simp:object_slot_initialised_lookup cap_transform_def cap_object_simps update_cap_object_def)
-  apply (clarsimp simp: object_at_def is_pd_def)
+  apply (clarsimp simp: object_slot_initialised_lookup cap_transform_def
+                        update_cap_object_def object_at_def is_pd_def)
   apply (clarsimp split:cdl_object.split_asm)
-  apply (rule hoare_chain)
-    apply (rule seL4_Page_Table_Map[where cnode_cap = si_cspace_cap
-      and root_size = si_cnode_size and ptr = pt_ptr and pd_ptr = pd_ptr])
-          apply (simp add:word_bits_def guard_equal_si_cspace_cap)+
-  prefer 2
-   apply (clarsimp simp:si_objects_def sep_conj_assoc sep_state_projection2_def)
-   apply (clarsimp simp: object_slot_initialised_def cdl_lookup_pd_slot_def
-     object_fields_empty_def object_initialised_general_def)
-    apply (clarsimp simp:root_tcb_def sep_conj_assoc update_slots_def)
-    apply (sep_cancel)+
-  apply (clarsimp simp: object_slot_empty_def object_fields_empty_def
-                        object_initialised_general_def si_objects_def cdl_lookup_pd_slot_def
+  apply (wp add: seL4_Page_Table_Map[where cnode_cap = si_cspace_cap
+                                       and root_size = si_cnode_size
+                                       and ptr = pt_ptr
+                                       and pd_ptr = pd_ptr,
+                                     sep_wandise])
+         apply (simp add: word_bits_def guard_equal_si_cspace_cap)+
+  apply (clarsimp simp: si_objects_def  sep_state_projection2_def object_slot_empty_def
+                        object_fields_empty_def object_initialised_general_def cdl_lookup_pd_slot_def
                         root_tcb_def update_slots_def)
   apply sep_cancel+
-  apply (drule sep_map_c_sep_map_s)
-  apply (simp add:object_default_state_def object_type_def default_object_def object_slots_def)
-   apply (simp add:empty_cap_map_shiftr_NullCap)
-   apply (erule sep_any_imp)
-  done
-
-lemma valid_vm_rights_rw:
- "validate_vm_rights ({AllowRead, AllowWrite} \<inter> rights) = validate_vm_rights rights"
-  apply (rule set_eqI)
-  apply (clarsimp simp:validate_vm_rights_def)
-  done
-
-lemma seL4_Section_Map_object_initialised_sep:
-  "\<lbrace>\<guillemotleft>object_slot_empty spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
-    (si_cnode_id , offset sel4_section si_cnode_size) \<mapsto>c (FrameCap dev section_ptr {AllowRead, AllowWrite} n Real None) \<and>*
-    (si_cnode_id , offset sel4_pd si_cnode_size) \<mapsto>c (PageDirectoryCap pd_ptr Real None) \<and>*
-    si_objects \<and>* R\<guillemotright> and
-  K(pd_at spec_pd_ptr spec \<and>
-    opt_cap (spec_pd_ptr,unat (vaddr >> 20)) spec
-      = Some (FrameCap False spec_section_ptr (validate_vm_rights rights) n Fake None) \<and>
-
-    sel4_section < 2 ^ si_cnode_size \<and>
-    sel4_pd < 2 ^ si_cnode_size \<and>
-    (n = 20 \<or> n = 24) \<and>
-
- (* object ids mapping *)
-    t spec_pd_ptr = Some pd_ptr \<and>
-    t spec_section_ptr = Some section_ptr)\<rbrace>
-     seL4_Page_Map sel4_section sel4_pd vaddr rights vmattribs
-   \<lbrace>\<lambda>rv. \<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
-   (si_cnode_id , offset sel4_section si_cnode_size) \<mapsto>c (FrameCap dev section_ptr {AllowRead, AllowWrite} n Real None) \<and>*
-   (si_cnode_id , offset sel4_pd si_cnode_size) \<mapsto>c (PageDirectoryCap pd_ptr Real None) \<and>*
-   si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (clarsimp simp:object_slot_initialised_lookup cap_transform_def cap_object_simps
-    update_cap_object_def update_cap_objects_def valid_vm_rights_rw)
-  apply (clarsimp simp: object_at_def is_pd_def)
-  apply (clarsimp simp: cap_type_def split:cdl_object.split_asm)
-  apply (rule hoare_chain)
-    apply (rule seL4_Section_Map_wp[where cnode_cap = si_cspace_cap
-      and root_size = si_cnode_size and frame_ptr = section_ptr and rights = "{AllowRead, AllowWrite}"])
-          apply (simp add:word_bits_def guard_equal_si_cspace_cap)+
-  prefer 2
-   apply (clarsimp simp: object_slot_initialised_def cdl_lookup_pd_slot_def
-     object_fields_empty_def object_initialised_general_def)
-   apply (clarsimp simp:si_objects_def sep_conj_assoc sep_state_projection2_def)
-   apply (clarsimp simp:root_tcb_def sep_conj_assoc update_slots_def valid_vm_rights_rw)
-   apply (sep_erule_concl refl_imp)+
-   apply (assumption)
-  apply (clarsimp simp: object_slot_empty_def object_fields_empty_def
-    object_initialised_general_def si_objects_def cdl_lookup_pd_slot_def
-    root_tcb_def update_slots_def)
-  apply sep_cancel+
-  apply (drule sep_map_c_sep_map_s)
-  apply (simp add:object_default_state_def object_type_def
-    default_object_def object_slots_def)
-   apply (simp add:empty_cap_map_shiftr_NullCap)
-  apply (erule sep_any_imp)
-  done
+  apply (sep_drule sep_map_c_sep_map_s)
+   apply (fastforce simp: object_default_state_def object_type_def default_object_def
+                          object_slots_def empty_cap_map_shiftr_NullCap)
+  by sep_solve
 
 lemma assert_opt_validI:
   assumes w: "\<And>a. r = Some a \<Longrightarrow> \<lbrace>P\<rbrace> f a \<lbrace>Q\<rbrace>"
@@ -221,35 +179,6 @@ lemma assert_opt_validI:
   using w
   by (clarsimp simp:assert_opt_def split:option.split)
 
-lemma well_formed_cap_obj_match_frame:
-  "\<lbrakk> well_formed spec;
-     cdl_objects spec ptr = Some (Frame frame);
-     opt_cap cap_ref spec = Some cap;
-     cap_has_object cap;
-     cap_object cap = ptr\<rbrakk>
-  \<Longrightarrow> \<exists>is_real dev. cap = FrameCap dev ptr (validate_vm_rights (cap_rights cap)) (cdl_frame_size_bits frame) is_real None"
-  apply (case_tac cap_ref, clarsimp)
-  apply (frule (1) well_formed_well_formed_cap', simp)
-  apply (frule (3) well_formed_types_match)
-  apply (fastforce simp: well_formed_cap_def object_type_def cap_type_def cap_object_def cap_has_object_def
-                         cap_rights_def validate_vm_rights_def vm_read_write_def  vm_read_only_def
-                  split: cdl_cap.splits)
-   done
-
-lemma well_formed_cap_obj_match_pt:
-  "\<lbrakk>well_formed spec; pt_at (cap_object cap) spec;
-   opt_cap cap_ref spec = Some cap;
-   cap_has_object cap\<rbrakk>
-  \<Longrightarrow> \<exists>is_real. cap = PageTableCap (cap_object cap) is_real None"
-  apply (case_tac cap_ref, clarsimp)
-  apply (frule (1) well_formed_well_formed_cap', simp)
-  apply (frule (2) well_formed_cap_object, clarsimp)
-  apply (frule (3) well_formed_types_match)
-  apply (clarsimp simp: well_formed_cap_def object_type_def cap_type_def cap_object_def
-                        object_at_def is_pt_def
-                 split: cdl_object.splits cdl_cap.splits)
-  done
-
 lemma sep_caps_at_split: "a \<in> A \<Longrightarrow>
   si_caps_at t orig_caps spec dev A = (
   si_cap_at t orig_caps spec dev a \<and>* si_caps_at t orig_caps spec dev (A - {a}))"
@@ -259,227 +188,367 @@ lemma sep_caps_at_split: "a \<in> A \<Longrightarrow>
   apply (simp add:insert_absorb)
   done
 
-lemma map_page_in_pd_wp:
-  "\<lbrakk>well_formed spec; pd_at spec_pd_ptr spec\<rbrakk>
-    \<Longrightarrow>
-    \<lbrace>\<guillemotleft>object_slot_empty spec t spec_pd_ptr (unat (shiftr vaddr 20)) \<and>*
-      si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-      si_objects \<and>* R\<guillemotright> and
-      K ((pt_at spec_pt_section_ptr spec \<longrightarrow>
-          opt_cap (spec_pd_ptr, unat (shiftr vaddr 20)) spec = Some (PageTableCap spec_pt_section_ptr Fake None)) \<and>
-         (frame_at spec_pt_section_ptr spec \<longrightarrow>
-             (\<exists>n. (n = 20 \<or> n = 24) \<and>
-                   opt_cap (spec_pd_ptr, unat (shiftr vaddr 20)) spec =
-                   Some (FrameCap False spec_pt_section_ptr (validate_vm_rights rights) n Fake None))))\<rbrace>
-    map_page spec orig_caps spec_pt_section_ptr spec_pd_ptr rights vaddr
-    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (shiftr vaddr 20)) \<and>*
-          si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-          si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (clarsimp simp: map_page_def dest!:domE)
-  apply (frule (1) object_at_real_object_at)
-  apply (intro assert_opt_validI)
-  apply (subgoal_tac "spec_pd_ptr \<in> {obj_id. real_object_at obj_id spec}")
-   apply (subst sep_caps_at_split [where t = t and orig_caps = orig_caps and spec = spec and
-          a = spec_pd_ptr and A = "{obj_id. real_object_at obj_id spec}"], simp)+
-   apply clarsimp
-   apply (intro conjI impI)
-    apply (clarsimp simp: object_at_def is_pt_def is_frame_def
-                   split: cdl_object.split_asm)
-    apply (frule (1) object_at_real_object_at [where obj_id=spec_pt_section_ptr])
-    apply (subgoal_tac "spec_pt_section_ptr \<in> {obj_id. real_object_at obj_id spec} - {spec_pd_ptr}")
-     apply (subst sep_caps_at_split [where t = t and orig_caps = orig_caps and spec = spec and
-                  a = spec_pt_section_ptr and A = "{obj_id. real_object_at obj_id spec} - {spec_pd_ptr}"], assumption)+
-     apply (rule hoare_name_pre_state)
-     apply (clarsimp simp: si_cap_at_def sep_conj_exists)
-     apply (rule hoare_pre)
-      apply wp
-      apply (rule hoare_strengthen_post [OF seL4_Section_Map_object_initialised_sep[where t = t]], simp+)
-      apply (clarsimp simp:object_at_def is_frame_def is_pd_def)
-      apply (simp split:cdl_object.split_asm add:object_type_def)
-      apply (simp add:default_cap_def)
-      apply (drule(2) well_formed_cap_obj_match_frame)
-        apply (simp add: cap_has_object_def)
-       apply (simp add: cap_object_simps)
-      apply (clarsimp simp: offset_slot_si_cnode_size' sep_conj_assoc)
-      apply sep_solve
-     apply (clarsimp simp:object_at_def is_frame_def is_pd_def)
-     apply (simp split:cdl_object.split_asm add:object_type_def)
-     apply (simp add:default_cap_def)
-     apply (drule(2) well_formed_cap_obj_match_frame)
-       apply (simp add: cap_has_object_def)
-      apply (simp add:cap_object_simps)
-     apply (clarsimp simp:offset_slot_si_cnode_size')
-     apply (rule conjI)
-      apply sep_solve
-     apply fastforce
-    apply (clarsimp simp: object_at_def opt_object_def object_type_is_object)
-   apply (frule (1) object_at_real_object_at [where obj_id=spec_pt_section_ptr])
-   apply (subgoal_tac "spec_pt_section_ptr \<in> {obj_id. real_object_at obj_id spec} - {spec_pd_ptr}")
-    apply (subst sep_caps_at_split [where t = t and orig_caps = orig_caps and spec = spec and
-                 a = spec_pt_section_ptr], assumption)+
-    apply (rule hoare_name_pre_state)
-    apply (clarsimp simp:si_cap_at_def sep_conj_exists)
-    apply (rule hoare_pre)
-     apply wp
-     apply (rule hoare_strengthen_post [OF seL4_PageTable_Map_object_initialised_sep [where t = t]], simp+)
-     apply (clarsimp simp:object_at_def is_frame_def is_pd_def is_pt_def)
-     apply (simp split:cdl_object.split_asm add:object_type_def)
-     apply (simp add:default_cap_def offset_slot_si_cnode_size')
-     apply (clarsimp simp:sep_conj_assoc)
-     apply sep_solve
-    apply (clarsimp simp:object_at_def is_frame_def is_pd_def is_pt_def)
-    apply (simp split:cdl_object.split_asm add:object_type_def)
-    apply (simp add:default_cap_def offset_slot_si_cnode_size')
-    apply (rule conjI)
-     apply sep_solve
-    apply fastforce
-   apply (clarsimp simp: object_at_def opt_object_def object_type_is_object)
-  apply (clarsimp simp:object_at_def)
-  done
-
-lemma well_formed_frame_in_pt:
-  "\<lbrakk>well_formed spec; opt_cap (pt, pt_slot) spec = Some frame_cap; frame_cap \<noteq> NullCap; pt_at pt spec\<rbrakk>
-  \<Longrightarrow> \<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and>
-           (sz = 12 \<or> sz = 16) \<and>
-           is_fake_vm_cap frame_cap"
-  apply (clarsimp simp: well_formed_def object_at_def)
-  apply (drule_tac x = pt in spec)
-  apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
-                 split: option.split_asm)
-  done
-
-lemma well_formed_frame_in_pd:
-  "\<lbrakk>well_formed spec; opt_cap (pd, pt_slot) spec = Some frame_cap; pd_at pd spec; is_frame_cap frame_cap \<rbrakk> \<Longrightarrow>
-  (\<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and> (sz = 20 \<or> sz = 24)) \<and> is_fake_vm_cap frame_cap \<and> \<not> is_device_cap frame_cap"
-  apply (clarsimp simp: well_formed_def object_at_def)
-  apply (drule_tac x = pd in spec)
-  apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
-                 split: option.split_asm)
-  apply (drule_tac x = pt_slot in spec)
-  apply (drule_tac x = frame_cap in spec)
-  apply (clarsimp simp: is_fake_pt_cap_def cap_type_def
-                 split: cdl_cap.splits)
-  apply (clarsimp simp: cap_at_def opt_cap_def slots_of_def opt_object_def
-              simp del: split_paired_All)
-  apply (drule_tac x = pd in spec)
-  apply (drule_tac x = pt_slot in spec)
+lemma duplicate_frame_cap_sep:
+  "\<lbrace>\<guillemotleft>(si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
+    si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R\<guillemotright> and K (
+    well_formed spec \<and>
+    unat free_cptr < 2 ^ si_cnode_size \<and>
+    frame_at obj_id spec)\<rbrace>
+      duplicate_cap spec orig_caps (obj_id, free_cptr)
+  \<lbrace>\<lambda>_.
+   \<guillemotleft>si_cap_at t (map_of [(obj_id, free_cptr)]) spec dev obj_id
+    \<and>* si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec}
+    \<and>* si_objects
+    \<and>* R\<guillemotright>\<rbrace>"
+  apply (wp sep_wp: duplicate_cap_sep_general[
+        where free_cptr=free_cptr and
+          free_cptrs="[free_cptr]" and
+          obj_ids="obj_id # (sorted_list_of_set (dom (cdl_objects spec) - {obj_id}))" and
+          spec=spec and
+          obj_id=obj_id and
+          obj_filter=frame_at])
+  apply (clarsimp simp: object_at_def wf_obj_filter_frame_at, intro conjI)
+   apply sep_solve
   apply fastforce
   done
 
-lemma map_page_directory_slot_wp:
-  "\<lbrace>\<guillemotleft>object_slot_empty spec t spec_pd_ptr slot \<and>*
-     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-     well_formed spec \<and>
-    slot < 0x1000 \<and>
-    pd_at spec_pd_ptr spec)\<rbrace>
-    map_page_directory_slot spec orig_caps spec_pd_ptr slot
-    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t spec_pd_ptr slot \<and>*
-         si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (clarsimp simp: map_page_directory_slot_def)
-  apply (rule assert_opt_validI)
-  apply (rule hoare_name_pre_state)
-  apply wp
-   apply (rule hoare_strengthen_post[OF map_page_in_pd_wp[where t = t]], simp+)
-   apply (simp add:pt_size_def small_frame_size_def)
-   apply (subst (asm) shiftl_shiftr_id)
-     apply simp+
-    apply (rule word_of_nat_less)
-    apply (clarsimp simp:si_cap_at_def sep_conj_exists si_cnode_size_def)
-   apply (simp add: unat_of_nat_eq)
+lemma si_caps_at_take_2:
+  "\<lbrakk>well_formed spec;
+    pd_at spec_pd_ptr spec;
+    frame_at spec_pt_section_ptr spec\<rbrakk>
+   \<Longrightarrow> si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} =
+           (si_cap_at t orig_caps spec dev spec_pd_ptr \<and>*
+            si_cap_at t orig_caps spec dev spec_pt_section_ptr \<and>*
+            si_caps_at t orig_caps spec dev ({obj_id. real_object_at obj_id spec} -
+                                                      {spec_pd_ptr} - {spec_pt_section_ptr}))"
+  apply (frule (1) object_at_real_object_at)
+  apply (frule (1) object_at_real_object_at[where obj_id=spec_pt_section_ptr])
+  apply (clarsimp simp: object_at_def is_pd_def is_frame_def is_pt_def split: cdl_object.split_asm)
+  by (metis sep_caps_at_split[where a="spec_pd_ptr"]
+            sep_caps_at_split[where a="spec_pt_section_ptr"]
+            cdl_object.exhaust mem_Collect_eq member_remove option.inject remove_def)
+
+lemma si_caps_at_take_2_not_object_at:
+  "\<lbrakk>well_formed spec;
+    cdl_objects spec spec_pd_ptr = Some pd;
+    is_pd pd;
+    cdl_objects spec spec_pt_section_ptr = Some frame;
+    is_frame frame\<rbrakk>
+   \<Longrightarrow> si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} =
+           (si_cap_at t orig_caps spec dev spec_pd_ptr \<and>*
+            si_cap_at t orig_caps spec dev spec_pt_section_ptr \<and>*
+            si_caps_at t orig_caps spec dev ({obj_id. real_object_at obj_id spec} -
+                                                      {spec_pd_ptr} - {spec_pt_section_ptr}))"
+  by (erule si_caps_at_take_2; fastforce simp: object_at_def)
+
+lemma si_caps_at_take_2':
+  "\<lbrakk>well_formed spec;
+      pd_at spec_pd_ptr spec;
+      pt_at spec_pt_section_ptr spec \<rbrakk>
+   \<Longrightarrow> si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} =
+           (si_cap_at t orig_caps spec dev spec_pd_ptr \<and>*
+            si_cap_at t orig_caps spec dev spec_pt_section_ptr \<and>*
+            si_caps_at t orig_caps spec dev ({obj_id. real_object_at obj_id spec} -
+                                                      {spec_pd_ptr} - {spec_pt_section_ptr}))"
+  apply (frule (1) object_at_real_object_at)
+  apply  (frule (1) object_at_real_object_at[where obj_id=spec_pt_section_ptr],
+          clarsimp simp: object_at_def is_pd_def is_frame_def is_pt_def,
+          simp split: cdl_object.split_asm,
+          subst sep_caps_at_split[where a="spec_pd_ptr"], fastforce,
+          subst sep_caps_at_split[where a="spec_pt_section_ptr"]; fastforce)
+  done
+
+lemma frame_at_default_cap[simp]:
+  "well_formed spec \<Longrightarrow>
+   is_frame frame \<Longrightarrow>
+   cdl_objects spec (cap_object frame_cap) = Some frame \<Longrightarrow>
+   opt_cap (parent_id, slot) spec = Some frame_cap \<Longrightarrow>
+   is_fake_frame_cap frame_cap \<Longrightarrow>
+   t (cap_object frame_cap) = Some ptr' \<Longrightarrow>
+   default_cap (object_type frame) {ptr'} (object_size_bits frame) False
+     = conjure_real_frame_cap frame_cap t"
+  apply (clarsimp simp: si_caps_at_take_2  si_cap_at_def object_type_is_object object_at_def
+                        default_cap_def object_type_def wf_frame_cap_frame_size_bits
+                        offset_slot_si_cnode_size' vm_read_write_def si_objects_def)
+  apply (clarsimp simp: is_frame_def split: cdl_object.splits)
+  apply (clarsimp split: cdl_cap.splits cdl_frame_cap_type.splits option.splits)
+  apply (drule_tac frame=x8 in wf_frame_cap_frame_size_bits)
+  by (fastforce simp: vm_read_write_def conjure_real_frame_cap_def dev_of_def)+
+
+lemma is_frame_default_cap[simp]:
+  "well_formed spec \<Longrightarrow>
+   frame_at (cap_object frame_cap) spec \<Longrightarrow>
+   cdl_objects spec (cap_object frame_cap) = Some obj \<Longrightarrow>
+   opt_cap (parent_id, slot) spec = Some frame_cap \<Longrightarrow>
+   is_fake_frame_cap frame_cap \<Longrightarrow>
+   t (cap_object frame_cap) = Some ptr' \<Longrightarrow>
+   default_cap (object_type obj) {ptr'} (object_size_bits obj) False
+     = conjure_real_frame_cap frame_cap t"
+  by (fastforce dest!: frame_at_default_cap simp: object_at_def)
+
+lemma pt_slot_compute[simp]:
+  "pt_slot < 2 ^ 8 \<Longrightarrow> unat (pt_slot_of_vaddr (frame_vaddr_of_slots pd_slot pt_slot)) = pt_slot"
   apply (clarsimp simp:pt_size_def small_frame_size_def)
-  apply (intro conjI impI)
-     apply (simp add:shiftl_shiftr_id word_of_nat_less unat_of_nat_eq)
-    apply (simp add:shiftl_shiftr_id word_of_nat_less unat_of_nat_eq si_cnode_size_def)
-    apply (frule (2) well_formed_cap_obj_match_pt)
-     apply (frule (3) well_formed_pd)
-     apply (clarsimp simp: cap_has_object_def cap_type_def is_fake_pt_cap_def split: cdl_cap.splits)
-    apply (frule well_formed_pt_cap_is_fake_pt_cap)
-       apply simp+
-     apply (case_tac "cap_object a",clarsimp)
-    apply (clarsimp simp:is_fake_pt_cap_def split:cdl_cap.splits)
-    apply (case_tac is_real,simp+)[1]
-   apply (simp add:shiftl_shiftr_id word_of_nat_less unat_of_nat_eq si_cnode_size_def)
-   apply (clarsimp simp: object_at_def is_frame_def)
-   apply (clarsimp split: cdl_object.split_asm)
-   apply (frule (2) well_formed_cap_obj_match_frame)
-     apply (frule (1) well_formed_pd)
-       apply (clarsimp simp: object_at_def)
-      apply assumption
-     apply (clarsimp simp: cap_has_object_def cap_type_def is_fake_pt_cap_def split: cdl_cap.splits)
-    apply clarsimp
-   apply (drule well_formed_frame_in_pd)
-      apply simp+
-     apply (simp add:object_at_def)
-    apply (case_tac a,simp_all)
-    apply clarsimp
-   apply (clarsimp simp:is_fake_vm_cap_def split:cdl_cap.split_asm cdl_frame_cap_type.split_asm)
-  apply (frule object_slot_empty_initialised_NullCap [where obj_id=spec_pd_ptr and slot=slot and t=t])
-    apply (clarsimp simp: object_at_def object_type_is_object)
+  apply (rule of_nat_inverse)
+   apply (drule of_nat_mono_maybe[rotated,where 'a=32])
+    apply simp
+   apply word_bitwise
    apply simp
   apply simp
   done
 
-lemma well_formed_pd_slot_limited:
-  "\<lbrakk>well_formed spec;pd_at obj_id spec; slots_of obj_id spec slot = Some cap\<rbrakk>
-   \<Longrightarrow> slot < 4096"
-  apply (clarsimp simp:well_formed_def object_at_def)
-  apply (drule_tac x = obj_id in spec)
-  apply (clarsimp simp: is_pd_def object_type_simps object_default_state_def slots_of_def,
-              simp add: default_object_def object_type_simps opt_object_def object_slots_def empty_cap_map_def
-                 split: cdl_object.split_asm option.split_asm)
-  apply fastforce
+lemma pd_slot_compute_from_pt[simp]:
+  "pd_slot < 2 ^ 12 \<Longrightarrow>
+   pt_slot < 2 ^ 8 \<Longrightarrow>
+   unat (pd_slot_of_pt_vaddr (frame_vaddr_of_slots pd_slot pt_slot)) = pd_slot"
+  apply (clarsimp simp: cdl_lookup_pd_slot_def pt_size_def small_frame_size_def)
+  apply (rule of_nat_inverse)
+   apply (drule of_nat_mono_maybe[rotated,where 'a=32],simp)+
+   apply (subst is_aligned_add_or [where n=20])
+     apply (rule is_aligned_shiftl, simp)
+    apply (rule shiftl_less_t2n, simp+)
+   apply (clarsimp simp: shiftr_over_or_dist)
+   apply (subst shiftl_shiftr_id, simp+)
+   apply (clarsimp simp: limited_and_simps)
+   apply (subst le_mask_iff [THEN iffD1])
+    apply (clarsimp simp: mask_def plus_one_helper)
+   apply clarsimp
+  apply (clarsimp simp: word_bits_len_of)
   done
 
-lemma well_formed_pt_slot_limited:
-  "\<lbrakk>well_formed spec;pt_at obj_id spec; slots_of obj_id spec slot = Some cap\<rbrakk>
-   \<Longrightarrow> slot < 256"
-  apply (clarsimp simp:well_formed_def object_at_def)
-  apply (drule_tac x = obj_id in spec)
-  apply (clarsimp simp: is_pt_def object_type_simps object_default_state_def slots_of_def,
-              simp add: default_object_def object_type_simps opt_object_def object_slots_def empty_cap_map_def
-                 split: cdl_object.split_asm option.split_asm)
-  apply fastforce
+lemma pd_slot_compute_inverse[simp]:
+  "pd_slot < 2 ^ 12 \<Longrightarrow>
+   unat (pd_slot_of_pt_vaddr (pt_vaddr_of_pd_slot pd_slot)) = pd_slot"
+  apply (clarsimp simp: cdl_lookup_pd_slot_def pt_size_def small_frame_size_def)
+  apply (rule of_nat_inverse)
+   apply (drule of_nat_mono_maybe[rotated, where 'a=32], simp)+
+   apply (word_bitwise, clarsimp, clarsimp)
   done
 
+lemma object_slot_empty_translate_exists:
+  "(object_slot_empty spec t pt_id pt_slot) s \<Longrightarrow>
+   (object_slot_empty spec t pt_id pt_slot) s \<and> t pt_id \<noteq> None"
+  by (clarsimp simp: object_slot_empty_def object_initialised_general_def)
 
-lemma map_map_page_directory_slot_wp':
-  "\<lbrace>\<guillemotleft>object_slots_empty spec t obj_id \<and>*
-     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-  well_formed spec \<and> pd_at obj_id spec)\<rbrace>
-    mapM_x (map_page_directory_slot spec orig_caps obj_id)
-           (slots_of_list spec obj_id)
-    \<lbrace>\<lambda>_. \<guillemotleft>object_slots_initialised spec t obj_id \<and>*
+lemma object_slot_initialised_translate_exists:
+  "(object_slot_initialised spec t pt_id pt_slot) s \<Longrightarrow>
+   (object_slot_initialised spec t pt_id pt_slot) s \<and> t pt_id \<noteq> None"
+  by (clarsimp simp: object_slot_initialised_def object_initialised_general_def)
+
+lemma si_cap_at_translate_exists:
+ "si_cap_at t f spec dev page_id s \<Longrightarrow>
+  si_cap_at t f spec dev page_id s \<and> t page_id \<noteq> None"
+  by (clarsimp simp: si_cap_at_def)
+
+lemmas translate_exists = si_cap_at_translate_exists object_slot_initialised_translate_exists
+                          object_slot_empty_translate_exists
+
+lemma si_caps_at_less_si_cnode_size:
+  "(si_caps_at t orig_caps spec dev xs \<and>* R) s \<Longrightarrow>
+   orig_caps ptr = Some v \<Longrightarrow>
+   ptr \<in> xs \<Longrightarrow>
+   v < 2 ^ si_cnode_size"
+  by (clarsimp simp: sep_caps_at_split si_cap_at_def sep_conj_def)
+
+lemma si_caps_at_less_translate_exists:
+  "(si_caps_at t orig_caps spec dev xs \<and>* R) s \<Longrightarrow>
+  ptr \<in> xs \<Longrightarrow>
+  t ptr \<noteq> None"
+  by (clarsimp simp: sep_caps_at_split si_cap_at_def sep_conj_def)
+
+lemma map_page_wp:
+  "\<lbrakk>well_formed spec; pd_at spec_pd_ptr spec\<rbrakk> \<Longrightarrow>
+    \<lbrace>\<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
+      object_slot_empty spec t pt_id pt_slot \<and>*
+      (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
+      si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+      si_objects \<and>* R\<guillemotright> and
+      K (page_cap = fake_frame_cap False page_id (validate_vm_rights rights) n \<and>
+         (n = 12 \<or> n = (16 :: nat)) \<and>
+         opt_cap (spec_pd_ptr, pd_slot) spec = Some pt_cap \<and>
+         pt_cap = PageTableCap pt_id Fake None \<and>
+         opt_cap (pt_id, pt_slot) spec = Some page_cap \<and>
+         vaddr = frame_vaddr_of_slots pd_slot pt_slot \<and>
+         pt_slot < 2 ^ 8 \<and>
+         pd_slot < 2 ^ 12 \<and>
+         the (orig_caps spec_pd_ptr) < 2 ^ si_cnode_size \<and>
+         free_cptr < 2 ^ si_cnode_size)\<rbrace>
+    map_page spec orig_caps page_id spec_pd_ptr rights vaddr free_cptr
+    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t spec_pd_ptr (unat (vaddr >> 20)) \<and>*
+          object_slot_initialised spec t pt_id pt_slot \<and>*
+          (si_cnode_id, unat free_cptr) \<mapsto>c conjure_real_frame_cap page_cap t \<and>*
+          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+          si_objects \<and>* R\<guillemotright>\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (frule well_formed_pt_cap_pt_at[where cap=pt_cap],
+         fastforce, clarsimp simp: is_fake_pt_cap_def)
+  apply (elim conjE)
+  apply (clarsimp simp: map_page_def dest!: domE)
+  apply (wp)
+         apply (clarsimp simp: object_at_def)
+         apply (wp sep_wp: seL4_Page_Map_object_initialised_sep
+                             [where n=n and
+                                    spec=spec and
+                                    cap_obj="the (cdl_objects spec pt_id)" and
+                                    spec_pd_ptr=spec_pd_ptr and
+                                    pt_ptr="the (t pt_id)" and
+                                    pt_cap=pt_cap and
+                                    spec_page_ptr=page_id and
+                                    page_ptr="the (t page_id)" and
+                                    t=t and
+                                    pd_ptr="the (t spec_pd_ptr)"]
+                           duplicate_frame_cap_sep)+
+  apply clarsimp
+  apply (intro conjI, sep_cancel+, intro conjI)
+          apply (sep_simp si_caps_at_take_2 si_cap_at_def)
+          apply (clarsimp simp: offset_slot_si_cnode_size' vm_read_write_def
+                                conjure_real_frame_cap_def dev_of_def
+                                is_frame_default_cap[where frame_cap=page_cap])
+          apply sep_solve
+         apply (fastforce simp: object_at_def pt_size_def pt_has_slots
+                         intro: object_slots_object_default_state_NullCap')+
+  by (sep_map thms: translate_exists, fastforce simp: unat_less_2_si_cnode_size')+
+
+lemma map_page_in_pd_wp:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk> \<Longrightarrow>
+    \<lbrace>\<guillemotleft>object_slot_empty spec t pd_id pd_slot \<and>*
+      (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
+      si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+      si_objects \<and>* R\<guillemotright> and
+      K (    page_cap = fake_frame_cap False page_id (validate_vm_rights rights) n \<and>
+             (n = 20 \<or> n = (24 :: nat)) \<and>
+             pd_slot = unat (pd_slot_of_pt_vaddr vaddr) \<and>
+             opt_cap (pd_id, pd_slot) spec = Some page_cap \<and>
+             pd_slot < 2 ^ 12 \<and>
+             the (orig_caps pd_id) < 2 ^ si_cnode_size \<and>
+             free_cptr < 2 ^ si_cnode_size)\<rbrace>
+    map_page spec orig_caps page_id pd_id rights vaddr free_cptr
+    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t pd_id pd_slot \<and>*
+          (si_cnode_id, unat free_cptr) \<mapsto>c conjure_real_frame_cap page_cap t \<and>*
+          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+          si_objects \<and>* R\<guillemotright>\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (elim conjE)
+  apply (clarsimp simp: map_page_def dest!: domE)
+  apply (intro assert_opt_validI)
+  apply wp
+     apply (clarsimp simp: object_at_def)
+     apply (wp sep_wp: seL4_Section_Map_wp[where pd_ptr="the (t pd_id)" and
+                                                 frame_ptr="the (t page_id)" and
+                                                 cnode_cap=si_cspace_cap and
+                                                 root_size=si_cnode_size and
+                                                 n=n];
+            fastforce simp: word_bits_def intro!: guard_equal_si_cspace_cap)
+    apply (wp sep_wp: duplicate_frame_cap_sep)+
+  apply (clarsimp, intro conjI impI, clarsimp simp: si_objects_def cdl_lookup_pd_slot_def)
+   apply sep_cancel+
+   apply (sep_map thms: translate_exists)
+   apply (sep_simp si_cap_at_def object_at_def object_slot_empty_eq)
+   apply (sep_drule sep_map_c_sep_map_s)
+    apply (clarsimp simp: opt_cap_def object_default_state_def is_pd_def object_type_def
+                          default_object_def
+                    split: cdl_object.splits)
+    apply (clarsimp simp: object_slots_def empty_cap_map_def, fastforce)
+   apply sep_cancel+
+   apply (clarsimp simp: si_caps_at_take_2_not_object_at offset_slot_si_cnode_size' si_cap_at_def
+                         frame_at_default_cap[where frame_cap=page_cap] cap_object_def
+                         object_at_def conjure_real_frame_cap_def dev_of_def
+                         root_tcb_def update_slots_def)
+   apply sep_cancel+
+   apply (fastforce simp: object_slot_initialised_lookup shiftr_less cap_object_def
+                          validate_vm_rights_inter_rw)
+  by (fastforce simp: unat_less_2_si_cnode_size')
+
+lemma map_page_table_in_pd_wp:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk> \<Longrightarrow>
+    \<lbrace>\<guillemotleft>object_slot_empty spec t pd_id pd_slot \<and>*
+      si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
+      si_objects \<and>* R\<guillemotright> and
+      K ((n = 20 \<or> n = 24) \<and>
+         opt_cap (pd_id, pd_slot) spec = Some (PageTableCap spec_pt_section_ptr Fake None) \<and>
+         pd_slot < 2 ^ 12 \<and>
+         vaddr = pt_vaddr_of_pd_slot pd_slot)\<rbrace>
+    map_page_table spec orig_caps spec_pt_section_ptr pd_id rights vaddr
+    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t pd_id pd_slot \<and>*
           si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
           si_objects \<and>* R\<guillemotright>\<rbrace>"
   apply (rule hoare_gen_asm)
-  apply (subst object_slots_empty_decomp, simp+)
-  apply (subst object_slots_initialised_decomp, simp+)
-  apply (subst object_empty_slots_empty_initialised, simp)
-  apply (simp add:sep_conj_assoc)
-  apply (rule mapM_x_set_sep' [where I = "object_empty_slots_initialised spec t obj_id \<and>*
-                                          si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-                                          si_objects"
-                                and xs = "slots_of_list spec obj_id", unfolded sep_conj_assoc])
-    apply clarsimp
-   apply clarsimp
-  apply (wp sep_wp: map_page_directory_slot_wp [where t=t])
-  apply (clarsimp simp: well_formed_pd_slot_limited)
-  apply sep_solve
-  done
+  apply (clarsimp simp: map_page_table_def dest!: domE)
+  apply (intro assert_opt_validI)
+  apply wp
+    apply (clarsimp simp: opt_object_def object_at_def)
+    apply (wp sep_wp:
+              seL4_PageTable_Map_object_initialised_sep[where pt_ptr ="the (t spec_pt_section_ptr)"
+                                                        and   pd_ptr ="the (t pd_id)"])+
+  apply (clarsimp, intro conjI impI)
+         apply sep_cancel+
+         apply (sep_simp si_caps_at_take_2' si_cap_at_def offset_slot_si_cnode_size')
+         apply sep_solve
+        apply assumption+
+  by (sep_simp si_caps_at_less_si_cnode_size[rotated 2, OF pt_at_is_real]
+               si_caps_at_less_si_cnode_size[rotated 2, OF pd_at_is_real]
+               si_caps_at_less_translate_exists[rotated, OF pt_at_is_real]
+               si_caps_at_less_translate_exists[rotated, OF pd_at_is_real])+
 
-lemma object_fields_empty_initialised_pd:
-  "\<lbrakk>well_formed spec; pd_at obj_id spec\<rbrakk> \<Longrightarrow>
-   object_fields_empty spec t obj_id = object_fields_initialised spec t obj_id"
-  apply (clarsimp simp: object_at_def object_type_is_object)
-  apply (frule (1) well_formed_object_slots)
-  apply (clarsimp simp: object_fields_empty_def object_fields_initialised_def
-                        object_initialised_general_def object_at_def object_type_is_object)
-  apply (subst sep_map_f_object_size_bits_pd, simp+)
+lemma map_page_table_slot_wp:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<guillemotleft>object_slot_initialised spec t pd_id pd_slot \<and>*
+     object_slot_empty spec t (cap_object pt_cap) pt_slot \<and>*
+     (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
+     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+     si_objects \<and>* R\<guillemotright> and K (
+      opt_cap (pd_id, pd_slot) spec = Some pt_cap \<and>
+      pt_at (cap_object pt_cap) spec \<and>
+      opt_cap (pt_id, pt_slot) spec = Some page_cap \<and>
+      cptr_map (pt_id, pt_slot) = free_cptr \<and>
+      pt_cap = PageTableCap pt_id Fake None \<and>
+      ((page_cap = fake_frame_cap False page_id (validate_vm_rights rights) n \<and> (n = 12 \<or> n = 16))
+       \<or> page_cap = NullCap) \<and>
+      free_cptr < 2 ^ si_cnode_size \<and>
+      pd_slot < 2 ^ 12 \<and>
+      pt_slot < 2 ^ 8 \<and>
+      vaddr = pt_vaddr_of_pd_slot pd_slot)\<rbrace>
+    map_page_table_slot spec orig_caps pd_id pt_id vaddr cptr_map pt_slot
+    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t pd_id pd_slot \<and>*
+          object_slot_initialised spec t (cap_object pt_cap) pt_slot \<and>*
+          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+          si_objects \<and>* (si_cnode_id, unat free_cptr) \<mapsto>c conjure_real_frame_cap page_cap t \<and>* R\<guillemotright>\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (clarsimp simp: map_page_table_slot_def is_fake_pt_cap_def  dest!: domE split: cdl_cap.splits)
+  apply (intro conjI impI)
+   apply (wp sep_wp: map_page_wp[where n=n and page_cap=page_cap])
+   apply (clarsimp, intro conjI; clarsimp?)
+           apply sep_solve
+          apply (clarsimp simp: cap_rights_def)
+         apply fastforce+
+   apply (subst (asm) sep_caps_at_split[where a=pd_id], clarsimp simp: object_at_real_object_at)
+   apply (sep_simp si_cap_at_def)
+  apply (wp, clarsimp simp: conjure_real_frame_cap_def)
+  apply sep_cancel+
+  by (fastforce simp: object_slot_empty_initialised_NullCap object_at_def is_tcb_def)
+
+lemma map_page_directory_slot_page_wp:
+ "frame_at page_id spec \<Longrightarrow>
+  \<lbrace>\<guillemotleft>(object_slot_empty spec t pd_id pd_slot \<and>* (si_cnode_id, unat free_cptr) \<mapsto>c NullCap \<and>*
+    si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R)\<guillemotright> and
+   K (page_cap = fake_frame_cap False page_id (validate_vm_rights rights) n \<and> well_formed spec \<and>
+      pd_at pd_id spec \<and> (n = 20 \<or> n = 24) \<and> cptr_map (pd_id, pd_slot) = free_cptr \<and>
+      pd_slot = unat (pd_slot_of_pt_vaddr vaddr) \<and> opt_cap (pd_id, pd_slot) spec = Some page_cap \<and>
+      pd_slot < 2 ^ 12 \<and> the (orig_caps pd_id) < 2 ^ si_cnode_size \<and>
+      free_cptr < 2 ^ si_cnode_size)\<rbrace>
+    map_page_directory_slot spec orig_caps pd_id cptr_map pd_slot
+  \<lbrace>\<lambda>_. \<guillemotleft>(object_slot_initialised spec t pd_id pd_slot \<and>*
+        (si_cnode_id, unat free_cptr) \<mapsto>c conjure_real_frame_cap page_cap t \<and>*
+        si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>* si_objects \<and>* R)\<guillemotright>\<rbrace>"
+  apply (rule hoare_gen_asm)
+  apply (clarsimp simp: map_page_directory_slot_def)
+  apply (intro conjI impI)
+   apply (fastforce simp: object_at_def dest: not_frame_and_pt)
+  apply (wp sep_wp: map_page_in_pd_wp[where n=n])
+  apply clarsimp
+  apply (intro conjI)
+      apply sep_solve
+     apply (fastforce simp: cap_rights_def pt_size_def small_frame_size_def)+
   done
 
 lemma object_fields_empty_initialised_pt:
@@ -492,79 +561,305 @@ lemma object_fields_empty_initialised_pt:
   apply (subst sep_map_f_object_size_bits_pt, simp+)
   done
 
-(* MoveMe *)
-lemma object_default_state_frame [simp]:
-  "is_frame object \<Longrightarrow> object_default_state object = object"
-  by (clarsimp simp: object_default_state_def default_object_def
-                     object_type_is_object object_type_def
-              split: cdl_object.splits)
-
-(* MoveMe *)
-lemma spec2s_frame [simp]:
-  "is_frame object \<Longrightarrow> spec2s t object = object"
-  by (clarsimp simp: object_type_is_object object_type_def
-              split: cdl_object.splits)
-
-(* MoveMe *)
-lemma object_empty_initialised_frame:
-  "frame_at obj_id spec \<Longrightarrow>
-   object_empty spec t obj_id = object_initialised spec t obj_id"
-  by (clarsimp simp: object_empty_def object_initialised_def object_initialised_general_def object_at_def)
-
-
-lemma map_object_empty_initialised_frame:
-  "\<And>* map (object_empty spec t) [obj_id\<leftarrow>obj_ids . frame_at obj_id spec] =
-   \<And>* map (object_initialised spec t) [obj_id\<leftarrow>obj_ids . frame_at obj_id spec]"
-  apply (rule map_sep_list_conj_cong)
-  apply (clarsimp simp: object_empty_initialised_frame)
+lemma object_fields_empty_initialised_pd:
+  "\<lbrakk>well_formed spec; pd_at obj_id spec\<rbrakk> \<Longrightarrow>
+   object_fields_empty spec t obj_id = object_fields_initialised spec t obj_id"
+  apply (clarsimp simp: object_at_def object_type_is_object)
+  apply (frule (1) well_formed_object_slots)
+  apply (clarsimp simp: object_fields_empty_def object_fields_initialised_def
+                        object_initialised_general_def object_at_def object_type_is_object)
+  apply (subst sep_map_f_object_size_bits_pd, simp+)
   done
 
-lemma map_map_page_directory_slot_wp:
-  "\<lbrace>\<guillemotleft>object_empty spec t obj_id \<and>*
-     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-     well_formed spec \<and> pd_at obj_id spec)\<rbrace>
-    mapM_x (map_page_directory_slot spec orig_caps obj_id)
-           (slots_of_list spec obj_id)
-   \<lbrace>\<lambda>_.
-    \<guillemotleft>object_initialised spec t obj_id \<and>*
-     si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright>\<rbrace>"
+lemma pt_NullCap_empty_init:
+  "well_formed spec \<Longrightarrow>
+   pt_at obj_id spec \<Longrightarrow>
+   cap_at (\<lambda>x. x = NullCap) (obj_id, slot) spec \<Longrightarrow>
+   object_slot_empty spec t obj_id slot = object_slot_initialised spec t obj_id slot"
+  apply (rule object_slot_empty_initialised_NullCap)
+    apply fastforce
+   apply (clarsimp simp: object_at_def is_pt_def is_tcb_def  split: cdl_object.splits)
+   apply (metis cdl_object.exhaust)
+  apply (clarsimp simp: cap_at_def)
+  done
+
+lemma pd_NullCap_empty_init:
+  "well_formed spec \<Longrightarrow>
+   pd_at obj_id spec \<Longrightarrow>  cap_at (\<lambda>x. x = NullCap) (obj_id, slot) spec \<Longrightarrow>
+   object_slot_empty spec t obj_id slot = object_slot_initialised spec t obj_id slot"
+  apply (rule object_slot_empty_initialised_NullCap)
+    apply clarsimp
+   apply (clarsimp simp: object_at_def is_pd_def is_tcb_def  split: cdl_object.splits)
+   apply (metis cdl_object.exhaust)
+  apply (clarsimp simp: cap_at_def)
+  done
+
+(* FIXME: Auto-generate these kind of lemmas *)
+lemma rewrite_pt[simp]:
+  "is_pt object \<Longrightarrow>
+    (case object of Endpoint \<Rightarrow> f1 |
+                    Notification \<Rightarrow> f2 | Tcb x \<Rightarrow> f3 x | CNode x \<Rightarrow> f4 x |
+                    AsidPool x \<Rightarrow> f5 x | PageTable x \<Rightarrow> P  | PageDirectory x \<Rightarrow> f7 x |
+                    Frame x \<Rightarrow> f8 x | Untyped \<Rightarrow> f9 | IRQNode x \<Rightarrow> f10 x) = P"
+  apply (cases object; simp add: is_pt_def)
+  done
+
+lemma map_page_directory_slot_pt_wp:
+  "pt_at pt_id spec \<Longrightarrow>
+   \<lbrace>\<guillemotleft>object_slot_empty spec t pd_id slot \<and>*
+     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+     si_objects \<and>*
+     sep_map_list_conj ((\<lambda>x. (si_cnode_id, unat x) \<mapsto>c NullCap) o cptr_map o (Pair pt_id))
+                       [slot <- page_slots. cap_at ((\<noteq>) NullCap) (pt_id, slot) spec]  \<and>*
+     object_empty spec t pt_id \<and>* R\<guillemotright> and K (
+       (\<forall>n \<in> range cptr_map. n < 2 ^ si_cnode_size) \<and>
+       pt_cap = PageTableCap pt_id Fake None  \<and>
+       well_formed spec \<and>
+       slot < 0x1000 \<and> (n = 12 \<or> n = (16 :: nat)) \<and>
+       pd_at pd_id spec \<and>
+       page_slots = slots_of_list spec pt_id \<and>
+       opt_cap (pd_id, slot) spec = Some pt_cap)\<rbrace>
+    map_page_directory_slot spec orig_caps pd_id  cptr_map slot
+    \<lbrace>\<lambda>_. \<guillemotleft>sep_map_list_conj (\<lambda>x. (si_cnode_id, unat (cptr_map (pt_id, x)))
+                                 \<mapsto>c conjure_real_frame_cap (the_cap spec pt_id x) t)
+                            [slot <- page_slots. cap_at ((\<noteq>) NullCap) (pt_id, slot) spec] \<and>*
+          object_initialised spec t pt_id  \<and>* object_slot_initialised spec t pd_id slot \<and>*
+          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+          si_objects \<and>* R\<guillemotright>\<rbrace>"
   apply (rule hoare_gen_asm)
+  apply (clarsimp simp: map_page_directory_slot_def)
+  apply (rule hoare_name_pre_state)
+  apply (wp map_page_table_slot_wp[where pt_cap=pt_cap,
+                                   simplified sep_wp_simp, THEN sep_hoare_fold_mapM_x]
+            map_page_table_in_pd_wp[sep_wandise])+
+  apply (clarsimp, intro conjI impI)
+      apply sep_cancel+
+      apply (clarsimp simp: pt_size_def small_frame_size_def word_of_nat_less word_bits_def
+                            unat_of_nat32)
+      apply (sep_fold_cancel, rule sep_map_sep_foldI)
+       apply (clarsimp simp: map2_def comp_def object_empty_decomp object_initialised_decomp
+                             object_empty_slots_empty_initialised object_fields_empty_initialised_pt
+                             object_slots_initialised_decomp object_slots_empty_decomp sep_conj_ac)
+       apply sep_cancel+
+       apply (clarsimp simp: well_formed_finite sep.prod.union_diff2 sep_list_conj_sep_map_set_conj
+                             well_formed_distinct_slots_of_list
+                             sep_map_set_conj_set_cong
+                               [OF split_filter_set
+                                     [where xs="dom (slots_of pt_id spec)" and
+                                            P="\<lambda>slot. cap_at ((\<noteq>) NullCap) (pt_id, slot) spec"]])
+       apply sep_cancel+
+       apply (fastforce elim: sep_map_set_conj_match
+                        simp: pt_NullCap_empty_init not_cap_at_cap_not_at eq_commute)
+      apply clarsimp
+      apply (intro conjI)
+        apply (clarsimp simp: object_at_def cap_at_def)
+       apply clarsimp
+       apply (erule wf_cap_in_pt_is_frame; fastforce simp: cap_at_def)
+      apply (frule well_formed_slot_object_size_bits_pt[where obj_id=pt_id,
+                                                        simplified object_size_bits_def])
+  by (fastforce simp: cap_at_def opt_cap_def pt_size_def small_frame_size_def)+
+
+lemma map_page_directory_wp_expanded:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec; pd_slots = slots_of_list spec pd_id;
+    list_all (\<lambda>n. n < 2 ^ 12) pd_slots; \<forall>ptr. cptr_map ptr < 2 ^ si_cnode_size;
+    the (orig_caps pd_id) < 2 ^ si_cnode_size\<rbrakk> \<Longrightarrow>
+    \<lbrace>\<guillemotleft>si_objects \<and>*
+      si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+      \<And>* map (\<lambda>x.
+          let pt_id = get_obj pd_id x spec in
+          object_slot_empty spec t pd_id x \<and>*
+          object_empty spec t pt_id \<and>*
+          sep_map_set_conj (\<lambda>y. (si_cnode_id, unat (cptr_map (pt_id, y))) \<mapsto>c NullCap)
+                           {slot \<in> dom (slots_of pt_id spec).
+                             cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
+        [slot <- pd_slots. lookup_obj pd_id slot pt_at spec] \<and>*
+      \<And>* map (\<lambda>x.
+          let frame_id = get_obj pd_id x spec in
+          (si_cnode_id, unat (cptr_map (pd_id, x))) \<mapsto>c NullCap \<and>*
+          object_slot_empty spec t pd_id x)
+        [slot <- pd_slots. lookup_obj pd_id slot frame_at spec] \<and>*
+      R\<guillemotright>\<rbrace>
+      map_page_directory spec orig_caps cptr_map pd_id
+    \<lbrace>\<lambda>_. \<guillemotleft>si_objects \<and>*
+          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+          \<And>* map (\<lambda>x.
+              let pt_id = get_obj pd_id x spec in
+              object_slot_initialised spec t pd_id x \<and>*
+              object_initialised spec t pt_id \<and>*
+              sep_map_set_conj (\<lambda>y. (si_cnode_id, unat (cptr_map (pt_id, y)))
+                                    \<mapsto>c conjure_real_frame_cap (the_cap spec pt_id y) t)
+                               {slot \<in> dom (slots_of pt_id spec).
+                                 cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
+             [slot <- pd_slots. lookup_obj pd_id slot pt_at spec] \<and>*
+          \<And>* map (\<lambda>x.
+              let frame_id = get_obj pd_id x spec in
+              (si_cnode_id, unat (cptr_map (pd_id, x)))
+                \<mapsto>c conjure_real_frame_cap (the_cap spec pd_id x) t \<and>*
+              object_slot_initialised spec t pd_id x)
+             [slot <- pd_slots. lookup_obj pd_id slot frame_at spec] \<and>*
+          R\<guillemotright>\<rbrace>"
+  apply (clarsimp simp: map_page_directory_def Let_unfold)
+  apply wp
+    apply (rule sep_hoare_fold_mapM_x[OF map_page_directory_slot_pt_wp
+                                          [where t=t and
+                                                 page_slots="slots_of_list spec pt_id" and
+                                                 pt_id="get_obj pd_id slot spec"
+                                                 for pt_id slot,
+                                           simplified sep_wp_simp],
+                                          simplified fun_app_def])
+    apply (clarsimp simp: opt_cap_def cap_at_def)
+    apply (fastforce dest: Some_to_the)
+   apply (rule sep_hoare_fold_mapM_x[OF map_page_directory_slot_page_wp
+                                          [where t=t and
+                                                 rights="cap_rights cap" and
+                                                 n="cap_size_bits cap" and
+                                                 page_id="get_obj pd_id slot spec"
+                                                 for slot cap,
+                                           simplified sep_wp_simp],
+                                          simplified fun_app_def])
+   apply (clarsimp simp: cap_at_def)
+   apply (fastforce dest: Some_to_the)
   apply clarsimp
-  apply (subst object_empty_decomp)
-  apply (subst object_initialised_decomp)
-  apply (subst object_fields_empty_initialised_pd, assumption+)
-  apply (simp add: sep_conj_assoc)
-  apply (wp sep_wp: map_map_page_directory_slot_wp' [where t=t])
-  apply clarsimp
-  apply sep_solve
+  apply (sep_fold_cancel, rule sep_map_sep_foldI)
+   apply (clarsimp simp: cap_at_def)
+   apply sep_cancel+
+   apply (sep_fold_cancel, rule sep_map_sep_foldI)
+    apply (clarsimp simp: sep_list_conj_sep_map_set_conj well_formed_distinct_slots_of_list
+                          well_formed_finite)
+    apply sep_solve
+   apply (intro conjI)
+       apply (fastforce dest: Some_to_the)
+      apply (fastforce elim: list_all_spec)+
+   apply clarsimp
+   apply (erule wf_pt_in_pd_fake_and_none; fastforce)
+  apply (clarsimp, intro conjI)
+      apply (drule wf_frame_cap_in_pd; (fastforce simp: cap_at_def)?)
+     apply (drule wf_frame_cap_in_pd; (fastforce simp: cap_at_def)?)
+    apply (rule pd_slot_compute_inverse[symmetric], clarsimp)
+  by (fastforce simp: cap_at_def elim: list_all_spec)+
+
+lemma slots_of_pd_split:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk> \<Longrightarrow>
+   dom (slots_of pd_id spec) =
+    {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c \<noteq> NullCap \<and> pt_at (cap_object c) spec)
+                                              (pd_id, slot) spec} \<union>
+    {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c \<noteq> NullCap \<and> frame_at (cap_object c) spec)
+                                              (pd_id, slot) spec} \<union>
+    {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c = NullCap) (pd_id, slot) spec}"
+  apply (intro set_eqI iffI; clarsimp)
+   apply (clarsimp simp: slots_of_def opt_object_def cap_at_def opt_cap_object_slot_simp
+                   split: option.splits)
+   apply (fastforce dest: well_formed_pd_frame_or_pt)+
   done
 
-lemma set_asid_rewrite:
-  "\<lbrakk>pd_at obj_id spec;
-    cdl_objects spec obj_id = Some pd;
-    orig_caps obj_id = Some pd_offset;
-    pd_offset < 2 ^ si_cnode_size;
-    t obj_id = Some kobj_id\<rbrakk> \<Longrightarrow>
-   ((si_cnode_id, unat pd_offset) \<mapsto>c default_cap (object_type pd) {kobj_id} (object_size_bits pd) dev \<and>*
-    si_objects \<and>* R)
-    =
-   ((si_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
-     si_tcb_id \<mapsto>f Tcb (obj_tcb root_tcb) \<and>*
-    (si_cnode_id, unat seL4_CapInitThreadASIDPool) \<mapsto>c AsidPoolCap si_asidpool_id si_asidpool_base \<and>*
-    (si_cnode_id, unat pd_offset) \<mapsto>c PageDirectoryCap kobj_id Real None \<and>*
-     si_asidpool_id \<mapsto>f AsidPool empty_asid \<and>*
-    (\<And>*off \<in> {off. off < 2 ^ asid_low_bits}. (si_asidpool_id, off) \<mapsto>c -) \<and>*
-     si_cnode_id \<mapsto>f CNode (empty_cnode si_cnode_size) \<and>*
-    (si_tcb_id, tcb_cspace_slot) \<mapsto>c si_cspace_cap \<and>*
-    (si_cnode_id, unat seL4_CapInitThreadCNode) \<mapsto>c si_cnode_cap \<and>*
-    (si_cnode_id, unat seL4_CapIRQControl) \<mapsto>c IrqControlCap \<and>* R)"
-  apply (clarsimp simp: si_objects_def si_asid_def si_cap_at_def)
-  apply (clarsimp simp: sep_conj_assoc sep_conj_exists object_at_object_type default_cap_def)
-  apply (rule ext, rule)
-   apply sep_solve
-  apply sep_solve
+lemma wf_split_slots_of_pd:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk> \<Longrightarrow>
+   sep_map_set_conj P (dom (slots_of pd_id spec)) =
+    (sep_map_set_conj P
+      {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c \<noteq> NullCap \<and> pt_at (cap_object c) spec)
+                                                (pd_id, slot) spec} \<and>*
+     sep_map_set_conj P
+      {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c \<noteq> NullCap \<and> frame_at (cap_object c) spec)
+                                                (pd_id, slot) spec} \<and>*
+     sep_map_set_conj P
+      {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>c. c = NullCap) (pd_id, slot) spec})"
+  apply clarsimp
+  apply (subst slots_of_pd_split)
+    apply (clarsimp simp: sep.prod.union_disjoint well_formed_finite[where obj_id=pd_id]
+                          cap_at_def)+
+  apply (subst sep.prod.union_disjoint)
+     apply (clarsimp simp: well_formed_finite[where obj_id=pd_id])+
+   apply (intro set_eqI iffI; clarsimp)
+  apply (subst sep.prod.union_disjoint)
+     apply (clarsimp simp: well_formed_finite[where obj_id=pd_id])+
+   apply (intro set_eqI iffI; clarsimp)
+   apply (fastforce dest: well_formed_pd_frame_or_pt)
+  apply (clarsimp simp: sep_conj_ac)
+  done
+
+lemma wf_pd_pt_obj_inj:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec\<rbrakk>
+   \<Longrightarrow> inj_on (ref_obj spec pd_id)
+             {slot \<in> dom (slots_of pd_id spec). lookup_obj pd_id slot pt_at spec}"
+  supply object_type_is_object[simp]
+  apply (clarsimp simp: inj_on_def cap_ref_object_def object_at_def)
+  apply (frule_tac obj_id=pd_id and slot=y in well_formed_types_match)
+     apply fastforce+
+  using object_type_is_object(9) object_type_object_at(9) wf_pd_cap_has_object apply blast
+  apply clarsimp+
+  apply (frule_tac obj_id=pd_id and slot=x in well_formed_types_match, fastforce+)
+  using object_type_is_object(9) object_type_object_at(9) wf_pd_cap_has_object apply blast
+  apply (clarsimp simp: cap_type_def split: cdl_cap.splits)
+  apply (frule_tac obj_id=pd_id and obj_id'=pd_id and slot=x and slot'=y in
+                   well_formed_fake_pt_caps_unique)
+         apply fastforce+
+     apply (erule well_formed_pt_cap_is_fake_pt_cap, fastforce+)
+    apply (erule well_formed_pt_cap_is_fake_pt_cap, fastforce+)
+  done
+
+lemma sep_map_pd_slots_inj[simp]:
+  "well_formed spec \<Longrightarrow>
+   pd_at pd_id spec \<Longrightarrow>
+   (SETSEPCONJ x | x \<in> dom (slots_of pd_id spec) \<and> lookup_obj pd_id x pt_at spec.
+      P (cap_object (the_cap spec pd_id x))) =
+   sep_map_set_conj P
+     {obj. \<exists>slot. slot \<in> dom (slots_of pd_id spec) \<and>
+                  lookup_obj pd_id slot pt_at spec \<and>
+                  obj = cap_object (the_cap spec pd_id slot)}"
+  apply (subgoal_tac "{obj. \<exists>slot. slot \<in> dom (slots_of pd_id spec) \<and>
+                                   lookup_obj pd_id slot pt_at spec \<and>
+                                   obj = cap_object (the_cap spec pd_id slot)} =
+                      ref_obj spec pd_id ` {slot \<in> dom (slots_of pd_id spec).
+                                              lookup_obj pd_id slot pt_at spec}")
+   prefer 2
+   apply (clarsimp simp: cap_ref_object_def)
+   apply blast
+  apply clarsimp
+  apply (subst sep.prod.reindex)
+   apply (erule (1) wf_pd_pt_obj_inj)
+  apply (clarsimp simp: cap_ref_object_def)
+  done
+
+lemma opt_cap_cap_at_simp: "(opt_cap ref spec = Some cap) = cap_at (\<lambda>x. x = cap) ref spec"
+  by (clarsimp simp: cap_at_def)
+
+lemma map_page_directory_wp:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec; pd_slots = slots_of_list spec pd_id;
+    list_all (\<lambda>n. n < 2 ^ 12) pd_slots; \<forall>ptr. cptr_map ptr < 2 ^ si_cnode_size;
+    the (orig_caps pd_id) < 2 ^ si_cnode_size\<rbrakk> \<Longrightarrow>
+     \<lbrace>\<guillemotleft>si_objects \<and>*
+       si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+       object_empty spec t pd_id \<and>*
+       frame_duplicates_empty cptr_map pd_id spec \<and>*
+       slots_in_object_empty (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec) pd_id spec t \<and>*
+       R\<guillemotright>\<rbrace>
+     map_page_directory spec orig_caps cptr_map pd_id
+     \<lbrace>\<lambda>_. \<guillemotleft>si_objects \<and>*
+           si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
+           object_initialised spec t pd_id \<and>*
+           frame_duplicates_copied cptr_map pd_id spec t \<and>*
+           slots_in_object_init (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec) pd_id spec t \<and>*
+           R\<guillemotright>\<rbrace>"
+  apply (wp map_page_directory_wp_expanded[sep_wandise])
+  apply sep_cancel+
+  apply (clarsimp simp: Let_unfold cap_at_def wf_split_slots_of_pd object_slots_empty_decomp
+                        object_empty_decomp[where spec_object_id=pd_id]
+                        sep_list_conj_sep_map_set_conj slots_in_object_empty_def
+                        frame_duplicates_empty_def cap_ref_object_def
+                        well_formed_distinct_slots_of_list well_formed_finite
+                        object_initialised_decomp[where spec_object_id=pd_id]
+                        frame_duplicates_copied_def object_slots_initialised_decomp
+                        object_fields_empty_initialised_pd object_empty_slots_empty_initialised)
+  apply sep_cancel+
+  apply (subst (asm) sep_map_set_conj_subst[OF pd_NullCap_empty_init];
+         clarsimp simp: opt_cap_cap_at_simp)
+  apply sep_cancel
+  apply (clarsimp simp: slots_in_object_init_def)
+  apply (fold cap_ref_object_def)
+  apply (erule sep_map_set_elim)
+   apply (clarsimp simp: image_def)
+   apply (intro set_eqI iffI; clarsimp simp: cap_at_def)
+  apply blast
   done
 
 lemma set_asid_wp:
@@ -585,8 +880,6 @@ lemma set_asid_wp:
   apply (rule hoare_grab_asm)+
   apply wpsimp
    apply (clarsimp simp: set_asid_def)
-   apply (subst set_asid_rewrite, assumption+)
-   apply (clarsimp simp: sep_conj_assoc)
    apply (wp add: hoare_drop_imps
             sep_wp: seL4_ASIDPool_Assign_wp [where
                     cnode_cap = si_cspace_cap and
@@ -602,57 +895,6 @@ lemma set_asid_wp:
   apply sep_solve
   done
 
-lemma map_map_page_directory_wp':
-  "\<lbrace>\<guillemotleft>(\<And>* pd_id \<in> {pd_id. pd_at pd_id spec}. object_empty spec t pd_id) \<and>*
-      si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-      si_objects \<and>* R\<guillemotright> and
-    K(well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
-    mapM_x (map_page_directory spec orig_caps)
-           [obj\<leftarrow>obj_ids. pd_at obj spec]
-    \<lbrace>\<lambda>rv. \<guillemotleft>(\<And>* pd_id \<in> {pd_id. pd_at pd_id spec}. object_initialised spec t pd_id) \<and>*
-          si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-          si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (rule mapM_x_set_sep' [where I = "si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>* si_objects",
-         simplified sep_conj_assoc])
-    apply simp
-   apply (fastforce simp: object_at_def)
-  apply (clarsimp simp: map_page_directory_def)
-  apply (wp map_map_page_directory_slot_wp, simp)
-  done
-
-lemma map_map_page_directory_wp:
-  "\<lbrace>\<guillemotleft>(\<And>* pt_id \<in> {pt_id. pt_at pt_id spec}. object_empty spec t pt_id) \<and>*
-     (\<And>* pd_id \<in> {pd_id. pd_at pd_id spec}. object_empty spec t pd_id) \<and>*
-      si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-      si_objects \<and>* R\<guillemotright> and K(
-      well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
-    mapM_x (map_page_directory spec orig_caps)
-           [obj\<leftarrow>obj_ids . pd_at obj spec]
-    \<lbrace>\<lambda>_.
-     \<guillemotleft>(\<And>* pt_id \<in> {pt_id. pt_at pt_id spec}. object_empty spec t pt_id) \<and>*
-      (\<And>* pd_id \<in> {pd_id. pd_at pd_id spec}. object_initialised spec t pd_id) \<and>*
-      si_caps_at t orig_caps spec dev {obj_id. real_object_at obj_id spec} \<and>*
-      si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (wp sep_wp: map_map_page_directory_wp' [where t=t], simp)
-  apply sep_solve
-  done
-
-lemma fake_pt_cap_rewrite:
-  "well_formed spec \<Longrightarrow>
-   {obj_id. pt_at obj_id spec \<and>
-           (\<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and> obj_id = cap_object cap)} =
-   {obj_id. \<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and> obj_id = cap_object cap}"
-  apply rule
-   apply clarsimp
-  apply (clarsimp simp: all_caps_def)
-  apply (frule (1) well_formed_cap_object, simp)
-  apply clarsimp
-  apply (drule (2) well_formed_types_match, clarsimp)
-  apply (fastforce simp: object_at_def object_type_is_object is_fake_pt_cap_is_pt_cap)
-  done
-
 lemma cap_transform_empty_cap_map [simp]:
   "cap_transform t \<circ>\<^sub>M empty_cap_map n = empty_cap_map n"
   apply (rule ext)
@@ -684,477 +926,254 @@ lemma object_empty_initialised_default_state:
   done
 
 lemma not_object_at:
-  "\<exists>object. cdl_objects spec obj_id = Some object \<Longrightarrow>
-  (\<not> object_at P obj_id spec) = object_at (\<lambda>obj. \<not>P obj) obj_id spec "
+  "(\<not> object_at P obj_id spec) \<Longrightarrow> cdl_objects spec obj_id = Some object \<Longrightarrow>
+   object_at (\<lambda>obj. \<not>P obj) obj_id spec "
   apply (clarsimp simp: object_at_def)
   done
 
-(* Each pt is either mapped in to a pd, or it is in a default state. *)
-lemma well_formed_pt_default_or_mapped:
-  "\<lbrakk>well_formed spec; pt_at obj_id spec;
-    \<forall>cap. is_fake_pt_cap cap \<longrightarrow>
-          cap \<in> all_caps spec \<longrightarrow> obj_id \<noteq> cap_object cap\<rbrakk> \<Longrightarrow>
-   object_at (\<lambda>obj. object_default_state obj = obj) obj_id spec"
+definition parent_obj_of :: "cdl_object_id \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> bool" where
+  "parent_obj_of parent_obj child_obj spec \<equiv>
+      (\<exists>slot \<in> dom (slots_of parent_obj spec).
+           cap_at (\<lambda>cap. cap_has_object cap \<and> cap_object cap = child_obj) (parent_obj, slot) spec)"
+
+definition pd_equiv_class :: "cdl_state \<Rightarrow> (cdl_object_id \<times> cdl_object_id) set" where
+  "pd_equiv_class spec \<equiv>
+    {(x,y). pt_at x spec \<and> pt_at y spec \<and>
+            (\<exists>obj. pd_at obj spec \<and> parent_obj_of obj x spec \<and> parent_obj_of obj y spec)}"
+
+lemma pd_equiv_sym:
+  "sym (pd_equiv_class spec)"
+  apply (clarsimp simp: sym_def pd_equiv_class_def)
+  by blast
+
+lemma pt_parents_eq:
+  "\<lbrakk>well_formed spec; pd_at obj_id spec; pd_at obj_id' spec; pt_at pt spec;
+    parent_obj_of obj_id pt spec; parent_obj_of obj_id' pt spec\<rbrakk>
+   \<Longrightarrow> obj_id = obj_id'"
+  apply (clarsimp simp: parent_obj_of_def cap_at_def)
+  apply (frule well_formed_fake_pt_caps_unique[where obj_id=obj_id and obj_id'=obj_id'])
+         apply assumption+
+     apply (metis (full_types) cap_has_object_not_NullCap cap_type_simps(8)
+                               well_formed_pt_cap_is_fake_pt_cap wf_pt_in_pd_fake_and_none)
+    apply (metis (full_types) cap_has_object_not_NullCap cap_type_simps(8)
+                              well_formed_pt_cap_is_fake_pt_cap wf_pt_in_pd_fake_and_none)
+   apply fastforce+
+  done
+
+lemma pd_equiv_trans:
+  "well_formed spec \<Longrightarrow> trans (pd_equiv_class spec)"
+  apply (clarsimp simp: trans_def pd_equiv_class_def)
+  apply (rule_tac x=obj in exI)
+  apply (clarsimp)
+  using pt_parents_eq by blast
+
+abbreviation (input)
+  "object_in_cap P ref spec \<equiv> cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> P (cap_object cap)) ref spec"
+
+(* Looking up PTs of a PD is injective, except when both have none *)
+lemma pd_pts_inj_or_empty:
+  "\<lbrakk>well_formed spec; pd_at x spec; pd_at y spec;
+    {obj. \<exists>slot. slot \<in> dom (slots_of x spec) \<and>
+                 object_in_cap (\<lambda>obj. pt_at obj spec) (x, slot) spec \<and> obj = ref_obj spec x slot} =
+    {obj. \<exists>slot. slot \<in> dom (slots_of y spec) \<and>
+                object_in_cap (\<lambda>obj. pt_at obj spec) (y, slot) spec \<and> obj = ref_obj spec y slot};
+    x \<noteq> y\<rbrakk> \<Longrightarrow>
+  {obj. \<exists>slot. slot \<in> dom (slots_of x spec) \<and>
+               object_in_cap (\<lambda>obj. pt_at obj spec) (x, slot) spec \<and> obj = ref_obj spec x slot} = {}"
+  apply (clarsimp simp: cap_at_def cap_ref_object_def)
+  apply (drule_tac x="cap_object cap" in eqset_imp_iff)
+  apply (frule pt_parents_eq[where obj_id = x and obj_id' = y];
+         fastforce simp: parent_obj_of_def cap_at_def wf_pd_cap_has_object)
+  done
+
+lemma wf_pd_equiv_parentD:
+  "\<lbrakk>(pt, pt') \<in> pd_equiv_class spec; well_formed spec; pd_at pd spec; parent_obj_of pd pt spec\<rbrakk>
+    \<Longrightarrow> parent_obj_of pd pt' spec"
+  apply (clarsimp simp: pd_equiv_class_def)
+  apply (frule_tac obj_id=obj and obj_id'=pd and pt=pt in pt_parents_eq; fastforce)
+  done
+
+lemma pd_equiv_ptsD: "pts \<in> pd_equiv_class spec \<Longrightarrow> pt_at (fst pts) spec \<and> pt_at (snd pts) spec"
+  by (clarsimp simp: pd_equiv_class_def split: prod.splits)
+
+(* Grouping PTs by their parent PD is the same as taking the PT children of each parent PD *)
+lemma pd_quotient_eq_pts_of_pds:
+  "well_formed spec \<Longrightarrow>
+   image (\<lambda>pd.{ref_obj spec pd slot | slot. slot \<in> dom (slots_of pd spec) \<and>
+                             object_in_cap (\<lambda>obj. pt_at obj spec) (pd, slot) spec})
+                             {obj. pd_at obj spec} - {{}} =
+   {x. pt_at x spec \<and> (\<exists>obj. pd_at obj spec \<and>
+     (\<exists>slot\<in>dom (slots_of obj spec). cap_at cap_has_object (obj, slot) spec
+                                    \<and> ref_obj spec obj slot = x))} // pd_equiv_class spec - {{}}"
+  apply (clarsimp simp: image_def quotient_def Image_def)
+  apply (intro set_eqI iffI; clarsimp simp: cap_at_def)
+   apply (guess_exI)
+   apply safe
+     apply (fastforce simp: wf_pd_cap_has_object cap_ref_object_def)
+    apply (clarsimp simp: pd_equiv_class_def cap_ref_object_def)
+    apply (guess_exI, clarsimp)
+    apply (intro conjI; fastforce simp: wf_pd_cap_has_object cap_ref_object_def
+                                        cap_at_def parent_obj_of_def)
+   apply (clarsimp simp: cap_ref_object_def)
+   apply (frule_tac pd=xa in wf_pd_equiv_parentD; clarsimp?)
+    apply (fastforce simp: wf_pd_cap_has_object cap_ref_object_def cap_at_def parent_obj_of_def)
+   apply (drule pd_equiv_ptsD, clarsimp simp: parent_obj_of_def cap_at_def)
+   apply (rule_tac x=slota in exI)
+   apply (fastforce simp: wf_pd_cap_has_object cap_ref_object_def
+                          pd_equiv_class_def cap_at_def parent_obj_of_def)
+  apply (rule_tac x=obj in exI)
+  apply (clarsimp simp: cap_ref_object_def)
+  apply (intro set_eqI iffI; clarsimp)
+   apply (frule_tac pd=obj and pt'=xa in wf_pd_equiv_parentD; clarsimp?)
+    apply (fastforce simp: parent_obj_of_def cap_at_def)
+   apply (drule pd_equiv_ptsD, clarsimp simp: parent_obj_of_def cap_at_def)
+   apply (rule_tac x=slota in exI)
+   apply (fastforce simp: wf_pd_cap_has_object cap_ref_object_def
+      pd_equiv_class_def cap_at_def parent_obj_of_def)
+  apply (clarsimp simp: pd_equiv_class_def)
+  apply (rule_tac x=obj in exI)
+  apply (clarsimp simp: parent_obj_of_def cap_at_def)
+  apply (metis (full_types) domI wf_pd_cap_has_object)
+  done
+
+lemma well_formed_pd_slots:
+  "\<lbrakk>well_formed spec; pd_at obj_id spec\<rbrakk> \<Longrightarrow>
+   \<forall>slot \<in> dom (slots_of obj_id spec). slot < 2 ^ 12"
+  by (fastforce simp: Ball_def elim: well_formed_pd_slot_limited)
+
+lemma well_formed_pt_not_in_pd_empty_init:
+ "\<lbrakk>well_formed spec; pt_at x spec;
+   (\<forall>obj. pd_at obj spec \<longrightarrow> (\<forall>slot\<in>dom (slots_of obj spec). cap_at cap_has_object (obj, slot) spec
+                         \<longrightarrow> ref_obj spec obj slot \<noteq> x))\<rbrakk>
+   \<Longrightarrow> object_empty spec t x = object_initialised spec t x"
+  apply (rule object_empty_initialised_default_state)
   apply (rule ccontr)
-  apply (subst (asm) not_object_at)
-   apply (clarsimp simp: object_at_def)
+  apply (drule not_object_at, fastforce)
   apply (frule (2) well_formed_cap_to_non_empty_pt)
   apply clarsimp
-  apply (clarsimp simp: object_at_def, rename_tac pt pd)
+  apply (erule_tac x=pd_id in allE, clarsimp)
+  apply (clarsimp simp: object_at_def)
   apply (case_tac "cap \<noteq> NullCap")
-   apply (frule (3) well_formed_types_match [symmetric])
-   apply (clarsimp simp: object_type_is_object)
-   apply (frule_tac obj_id=pd_id in well_formed_pt_cap_is_fake_pt_cap, assumption+)
-     apply (clarsimp simp: object_at_def object_type_is_object)
-    apply simp
-   apply (erule_tac x=cap in allE)
-   apply (fastforce simp: all_caps_def)
-  apply (clarsimp)
+   apply (frule well_formed_types_match[symmetric], fastforce+)
+   apply (fastforce dest: opt_cap_dom_slots_of
+                    simp: cap_at_def cap_ref_object_def object_at_def object_type_is_object)+
   done
 
-lemma object_empty_initialised_pt:
-  "\<lbrakk>well_formed spec; pt_at obj_id spec;
-   \<forall>cap. is_fake_pt_cap cap \<longrightarrow> cap \<in> all_caps spec \<longrightarrow> obj_id \<noteq> cap_object cap\<rbrakk>
-   \<Longrightarrow>
-   object_empty spec t obj_id = object_initialised spec t obj_id"
-  apply (rule object_empty_initialised_default_state)
-  apply (erule (2) well_formed_pt_default_or_mapped)
-  done
+lemma refl_on_pd_parent[simp]:
+  "refl_on {pt_id. pt_at pt_id spec \<and>
+                   (\<exists>obj. pd_at obj spec \<and> parent_obj_of obj pt_id spec)}
+           (pd_equiv_class spec)"
+  by (clarsimp simp: pd_equiv_class_def refl_on_def, fastforce)
 
-lemma map_object_empty_initialised_pt:
+lemma pt_parents_pd_pts_empty:
   "well_formed spec \<Longrightarrow>
-   (\<And>* obj_id \<in> {obj_id. pt_at obj_id spec \<and> (\<forall>cap. is_fake_pt_cap cap \<longrightarrow>
-                                                cap \<in> all_caps spec \<longrightarrow>
-                                                obj_id \<noteq> cap_object cap)}.
-          (object_empty spec t) obj_id)
-     =
-   (\<And>* obj_id \<in> {obj_id. pt_at obj_id spec \<and> (\<forall>cap. is_fake_pt_cap cap \<longrightarrow>
-                                                cap \<in> all_caps spec \<longrightarrow>
-                                                obj_id \<noteq> cap_object cap)}.
-           (object_initialised spec t) obj_id)"
-  apply (rule sep.prod.cong, clarsimp)
-  apply (clarsimp simp: object_empty_initialised_pt)
-  done
-
-
-lemma well_formed_pt_cap_pt_at:
-  "\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some cap; is_fake_pt_cap cap\<rbrakk>
-  \<Longrightarrow> pt_at (cap_object cap) spec"
-  apply (case_tac cap_ref, clarsimp)
-  apply (frule (1) well_formed_cap_object, simp, clarsimp)
-  apply (frule (2) well_formed_types_match, simp)
-  apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_at_def object_type_is_object)
-  done
-
-lemma pt_slot_compute:
-  "pt_slot < 2 ^ 8
-  \<Longrightarrow> unat (((of_nat pd_slot << pt_size + small_frame_size) + (of_nat pt_slot << small_frame_size) >> 12) && (0xFF::word32))
-  = pt_slot"
-  apply (clarsimp simp:pt_size_def small_frame_size_def)
-  apply (rule of_nat_inverse)
-   apply (drule of_nat_mono_maybe[rotated,where 'a=32])
-    apply simp
-   apply word_bitwise
-    apply simp
-  apply simp
-  done
-
-lemma cdl_lookup_pd_slot_compute:
-  "\<lbrakk>pd_slot < 2 ^ 12;pt_slot < 2 ^ 8\<rbrakk> \<Longrightarrow>
-   cdl_lookup_pd_slot pd_ptr
-   (((of_nat pd_slot::word32) << pt_size + small_frame_size) + (of_nat pt_slot << small_frame_size))
-  = (pd_ptr ,(of_nat pd_slot))"
-  apply (clarsimp simp: cdl_lookup_pd_slot_def pt_size_def small_frame_size_def)
-  apply (rule of_nat_inverse)
-   apply (drule of_nat_mono_maybe[rotated,where 'a=32],simp)+
-   apply (subst is_aligned_add_or [where n=20])
-     apply (rule is_aligned_shiftl, simp)
-    apply (rule shiftl_less_t2n, simp+)
-   apply (clarsimp simp: shiftr_over_or_dist)
-   apply (subst shiftl_shiftr_id, simp+)
-   apply (clarsimp simp: limited_and_simps)
-   apply (subst le_mask_iff [THEN iffD1])
-    apply (clarsimp simp: mask_def plus_one_helper)
-   apply clarsimp
-  apply (clarsimp simp: word_bits_len_of)
-  done
-
-lemma well_formed_frame_valid:
-  "\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some (FrameCap dev ptr seta sz real_type option)\<rbrakk>
-   \<Longrightarrow> validate_vm_rights seta = seta"
-  apply (case_tac cap_ref, clarsimp)
-  apply (frule (1) well_formed_well_formed_cap', simp)
-  apply (fastforce simp: well_formed_cap_def vm_read_write_def
-                         vm_read_only_def validate_vm_rights_def)
-  done
-
-lemma empty_cap_map_NullCap:
-  "pt_slot < 2 ^n \<Longrightarrow> empty_cap_map n pt_slot = Some NullCap"
-  by (simp add:empty_cap_map_def)
-
-(* FIXME: current cdl_init does not consider device caps *)
-lemma well_formed_opt_cap_nondevice:
-  "\<lbrakk>well_formed spec; opt_cap slot spec = Some cap\<rbrakk> \<Longrightarrow> \<not> is_device_cap cap"
-  by (simp add: well_formed_def cap_at_def del: split_paired_All)
-
-(***********************
- * Mapping page tables *
- ***********************)
-lemma map_page_in_pt_sep:
-  "\<lbrace>\<guillemotleft>object_slot_empty spec t (cap_object pt_cap) pt_slot \<and>*
-     object_slot_initialised spec t obj_id pd_slot \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-    well_formed spec \<and>
-    pd_at obj_id spec \<and>
-    opt_cap (obj_id, pd_slot) spec = Some pt_cap \<and>
-    is_fake_pt_cap pt_cap \<and>
-    opt_cap (cap_object pt_cap, pt_slot) spec = Some frame_cap \<and>
-    frame_cap \<noteq> NullCap \<and>
-    pt_slot < 2 ^ 8 \<and>
-    pd_slot < 2 ^ 12)\<rbrace>
-     map_page spec orig_caps (cap_object frame_cap)
-                obj_id (cap_rights frame_cap)
-                ((of_nat pd_slot << pt_size + small_frame_size) +
-                 (of_nat pt_slot << small_frame_size))
-  \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t (cap_object pt_cap) pt_slot \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>*
-         R\<guillemotright>\<rbrace>"
-  including no_pre
-  apply (rule hoare_gen_asm, clarsimp)
-  apply (simp add:map_page_def)
-  apply (rule assert_opt_validI)+
-  apply (frule (2) well_formed_pt_cap_pt_at[where cap = pt_cap])
-  apply (frule well_formed_frame_in_pt[where pt = "(cap_object pt_cap)"])
-    apply (simp+)[3]
-  apply (case_tac "frame_at (cap_object frame_cap) spec")
-   apply clarsimp
-
-  apply (frule (1) object_at_real_object_at)
-  apply (frule (1) object_at_real_object_at [where obj_id = "cap_object pt_cap"])
-  apply (frule (1) object_at_real_object_at [where obj_id = "cap_object frame_cap"])
-   apply (intro conjI)
-    apply (clarsimp simp: object_at_def is_pt_def is_frame_def,
-           simp split:cdl_object.splits)
-   apply clarsimp
-   apply wp
-   apply (clarsimp simp: object_at_def)
-   apply (subst sep_caps_at_split[where a = obj_id
-                                    and A = "{obj_id. real_object_at obj_id spec}"], fastforce)+
-   apply (subst sep_caps_at_split[where a = "cap_object pt_cap"
-                                    and A = "{obj_id. real_object_at obj_id spec} - {obj_id}"],
-          fastforce simp: object_type_is_object)+
-   apply (subst sep_caps_at_split[where a = "cap_object frame_cap"
-                                    and A = "{obj_id. real_object_at obj_id spec} - {obj_id} - {cap_object pt_cap}"],
-          fastforce simp: object_type_is_object)+
-   apply (rule hoare_name_pre_state)
-   apply (clarsimp simp: si_cap_at_def sep_conj_exists is_pd_def is_pt_def is_frame_def
-                  split: cdl_object.split_asm)
-   apply (clarsimp simp: object_type_def default_cap_def)
-   apply (clarsimp simp: object_slot_initialised_lookup)
-   apply (clarsimp simp: cap_type_def is_fake_vm_cap_def cap_object_simps
-                         cap_transform_def is_fake_pt_cap_def
-                  split: cdl_cap.split_asm cdl_frame_cap_type.split_asm)
-   apply (frule(1) well_formed_opt_cap_nondevice)
-   apply (rule hoare_pre)
-    apply (rule hoare_strengthen_post)
-     apply (rule_tac pd_ptr = kobj_id in seL4_Page_Map_wp[where cnode_cap = si_cspace_cap
-       and root_size = si_cnode_size and dev = False
-       and rights = "{AllowRead, AllowWrite}"])
-          apply (simp add:word_bits_def guard_equal_si_cspace_cap)+
-    apply (simp add:si_objects_def sep_conj_assoc pt_slot_compute)
-        apply (clarsimp simp: update_cap_object_def valid_vm_rights_rw cap_rights_def)
-    apply (sep_select 9, sep_cancel)
-    apply (sep_select 9,sep_cancel)
-    apply (clarsimp simp: update_cap_object_def valid_vm_rights_rw cap_rights_def)
-    apply (frule well_formed_frame_valid[rotated])
-     apply simp+
-    apply (subst sep_map_c_asid_simp)
-    apply sep_cancel
-    apply (simp add: cdl_lookup_pd_slot_compute)
-    apply (subst sep_map_c_asid_simp(2))
-    apply sep_cancel
-    apply (simp add:offset_slot_si_cnode_size')
-    apply sep_cancel
-    apply (simp add:root_tcb_def update_slots_def)
-    apply (sep_select 4,sep_cancel)
-    apply (sep_select 4,sep_cancel)
-    apply (drule (2)  well_formed_cap_obj_match_frame, simp)
-     apply (simp add:cap_object_simps)
-    apply clarsimp
-    apply (sep_select 2,sep_solve)
-   apply (clarsimp simp: si_objects_def root_tcb_def update_slots_def
-                         offset_slot_si_cnode_size' pt_slot_compute cdl_lookup_pd_slot_compute)
-   apply (drule (2) well_formed_cap_obj_match_frame, simp+)
-    apply (simp add:cap_object_simps)
-   apply (clarsimp simp:update_cap_object_def)
-   apply (subst (asm) sep_map_c_asid_simp(2))
-   apply (clarsimp simp: object_slot_empty_def object_fields_empty_def object_initialised_general_def)
-   apply (sep_drule sep_map_c_sep_map_s)
-    apply (simp add: object_default_state_def object_type_def
-                     default_object_def object_slots_def empty_cap_map_NullCap)
-   apply (simp add: fun_upd_def)
-   apply sep_solve
-  apply clarsimp
-  apply (clarsimp simp: is_pt_def object_at_def
-                 split: cdl_object.split_asm)
-  apply (drule (2) well_formed_types_match [where cap = frame_cap])
-   apply simp
-  apply (simp add:object_type_simps)
-  done
-
-lemma map_page_table_slot_wp:
-  "\<lbrace>\<guillemotleft>object_slot_empty spec t (cap_object page_cap) pt_slot \<and>*
-     object_slot_initialised spec t obj_id pd_slot \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-    well_formed spec \<and>
-    pd_at obj_id spec \<and>
-    is_fake_pt_cap page_cap \<and>
-    pt_slot < 256 \<and>
-    pd_slot < 2 ^ 12 \<and>
-    opt_cap (obj_id, pd_slot) spec = Some page_cap \<and>
-    opt_cap (cap_object page_cap, pt_slot) spec = Some frame_cap)\<rbrace>
-    map_page_table_slot spec orig_caps obj_id
-                       (cap_object page_cap)
-                       (of_nat pd_slot << pt_size + small_frame_size)
-                        pt_slot
-    \<lbrace>\<lambda>_. \<guillemotleft>object_slot_initialised spec t (cap_object page_cap) pt_slot \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (clarsimp simp: map_page_table_slot_def)
-  apply (wp map_page_in_pt_sep)
-  apply clarsimp
-  apply (subst (asm) object_slot_empty_initialised_NullCap, simp_all)
-  apply (clarsimp simp: object_at_def is_fake_pt_cap_def is_pd_def is_tcb_def)
-  apply (simp split:cdl_object.splits cdl_cap.splits)
-  apply (drule well_formed_types_match[where cap = page_cap],simp_all)
-  apply (simp add:object_type_def)
-  done
-
-lemma map_page_table_slots_wp'':
-  "\<lbrakk>well_formed spec;
-    pd_at obj_id spec;
-    fake_pt_cap_at (obj_id, pd_slot) spec;
-    opt_cap (obj_id, pd_slot) spec = Some page_cap\<rbrakk> \<Longrightarrow>
-   \<lbrace>\<guillemotleft>object_slots_empty spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-     object_slot_initialised spec t obj_id pd_slot \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright>\<rbrace>
-   mapM_x (map_page_table_slot spec orig_caps obj_id
-                              (cap_object page_cap)
-                              (of_nat pd_slot << pt_size + small_frame_size))
-          (slots_of_list spec (cap_object page_cap))
-   \<lbrace>\<lambda>_. \<guillemotleft>object_slots_initialised spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (frule well_formed_distinct_slots_of_list [where obj_id="cap_ref_object (obj_id, pd_slot) spec"])
-  apply (frule well_formed_finite [where obj_id="cap_ref_object (obj_id, pd_slot) spec"])
-  apply (subst object_slots_empty_decomp, simp+)
-  apply (subst object_slots_initialised_decomp, clarsimp+)
-  apply (subst object_empty_slots_empty_initialised, simp)
-  apply (clarsimp simp: sep_conj_assoc cap_ref_object_def cap_at_def)
-  apply (rule mapM_x_set_sep' [where I = "object_empty_slots_initialised spec t (cap_object page_cap) \<and>*
-                                          object_slot_initialised spec t obj_id pd_slot \<and>*
-                                          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-                                          si_objects", unfolded sep_conj_assoc], simp, clarsimp)
-  apply (frule is_fake_pt_cap_is_pt_cap)
-  apply (frule (1) well_formed_cap_object, clarsimp)
-  apply clarsimp
-  apply (frule (2) well_formed_types_match[where cap = page_cap], clarsimp)
-  apply (clarsimp simp: opt_cap_def)
-  apply (frule (2) well_formed_pd_slot_limited [where slot=pd_slot])
-  apply (frule well_formed_pt_slot_limited [where obj_id="cap_object page_cap"],
-         clarsimp simp: object_type_object_at, assumption)
-  apply (wp sep_wp: map_page_table_slot_wp [where t=t])
-  apply clarsimp
-  apply (rule conjI)
-   apply sep_solve
-  apply (simp add: opt_cap_def)
-  done
-
-lemma map_page_table_slots_wp':
-  "\<lbrace>\<guillemotleft>object_empty spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-     object_slot_initialised spec t obj_id pd_slot \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>*
-     R\<guillemotright> and K(
-     well_formed spec \<and>
-     pd_at obj_id spec \<and> fake_pt_cap_at (obj_id, pd_slot) spec \<and>
-     opt_cap (obj_id, pd_slot) spec = Some page_cap)\<rbrace>
-   mapM_x (map_page_table_slot spec orig_caps obj_id
-                               (cap_object page_cap)
-                               (of_nat pd_slot << pt_size + small_frame_size))
-          (slots_of_list spec (cap_object page_cap))
-   \<lbrace>\<lambda>_. \<guillemotleft>object_initialised spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>*
-   R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (subst object_empty_decomp)
-  apply (subst object_initialised_decomp)
-  apply (subst object_fields_empty_initialised_pt, simp+)
-   apply (clarsimp simp: cap_at_def)
-   apply (frule (1) well_formed_cap_object, clarsimp+)
-   apply (drule (2) well_formed_types_match, clarsimp)
-   apply (drule is_fake_pt_cap_is_pt_cap)
-   apply (clarsimp simp: object_at_def object_type_is_object cap_ref_object_def
-                  split: cdl_cap.splits)
-  apply (clarsimp simp: sep_conj_assoc)
-  apply (wp sep_wp: map_page_table_slots_wp'' [where t=t])
-  apply sep_solve
-  done
-
-lemma map_page_table_slots_wp:
-  "\<lbrace>\<guillemotleft>object_empty spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and K(
-    well_formed spec \<and>
-    pd_at obj_id spec \<and>
-    cdl_objects spec obj_id = Some obj \<and>
-    fake_pt_cap_at (obj_id, pd_slot) spec)\<rbrace>
-   map_page_table_slots spec orig_caps obj_id pd_slot
-    \<lbrace>\<lambda>_. \<guillemotleft>object_initialised spec t (cap_ref_object (obj_id, pd_slot) spec) \<and>*
-         object_slot_initialised spec t obj_id pd_slot \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm)
-  apply (clarsimp simp: map_page_table_slots_def)
-  apply (wp map_page_table_slots_wp', simp+)
-  done
-
-lemma object_initialised_slot_initialised:
-  "\<lbrakk> well_formed spec; slot \<in> dom (slots_of obj_id spec) \<rbrakk>
-  \<Longrightarrow> \<exists>F. object_initialised spec t obj_id
-       = (object_slot_initialised spec t obj_id slot \<and>* F)"
-  apply (frule well_formed_finite [where obj_id=obj_id])
-  apply (simp add: object_initialised_decomp_total)
-  apply (subst sep.prod.remove, assumption+)
-  by (metis sep_conj_assoc sep_conj_left_commute)
-
-lemma map_page_directory_page_tables_wp:
-  "\<lbrace>\<guillemotleft>(\<And>* slot\<in>set (slots_of_list spec obj_id).
-                     if fake_pt_cap_at (obj_id, slot) spec
-                     then (object_empty spec t (cap_ref_object (obj_id, slot) spec))
-                     else \<box>)  \<and>*
-     object_initialised spec t obj_id \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and
-    K(well_formed spec \<and> pd_at obj_id spec)\<rbrace>
-   map_page_directory_page_tables spec orig_caps obj_id
-   \<lbrace>\<lambda>_. \<guillemotleft>(\<And>* slot\<in>set (slots_of_list spec obj_id).
-                     if fake_pt_cap_at (obj_id, slot) spec
-                     then (object_initialised spec t (cap_ref_object (obj_id, slot) spec))
-                     else \<box>) \<and>*
-     object_initialised spec t obj_id \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm, clarsimp)
-  apply (frule well_formed_distinct_slots_of_list [where obj_id=obj_id])
-  apply (clarsimp simp: map_page_directory_page_tables_def)
-  apply (rule mapM_x_set_sep'[where I="object_initialised spec t obj_id \<and>*
-                                       si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-                                       si_objects",
-                                    unfolded sep_conj_assoc,simplified], simp+)
-  apply clarsimp
-  apply (rule conjI)
-   apply (clarsimp simp:sep_conj_assoc)
-   apply (frule object_initialised_slot_initialised[where obj_id = obj_id and t = t])
+   (SETSEPCONJ pd_id | pd_at pd_id spec.
+        slots_in_object_empty (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec) pd_id spec t) =
+   (SETSEPCONJ pt_id | pt_at pt_id spec \<and> (\<exists>obj. pd_at obj spec \<and> parent_obj_of obj pt_id spec).
+        object_empty spec t pt_id)"
+  apply (rule sym, subst sep_map_set_quotient_split[where R="pd_equiv_class spec"])
     apply fastforce
-   apply (clarsimp simp:sep_conj_assoc)
-   apply (frule slots_of_cdl_objects, clarsimp)
-   apply (wp sep_wp: map_page_table_slots_wp [where t=t], simp+)
-   apply (rule conjI)
-    apply sep_solve
-   apply simp
-  apply (clarsimp simp: map_page_table_slots_def)
-  apply wp
-  apply clarsimp
+   apply (rule equivI; clarsimp simp: pd_equiv_sym[simplified fun_app_def] pd_equiv_trans)
+  apply (clarsimp simp: slots_in_object_empty_def, rule sym, subst sep_map_set_squash)
+    apply clarsimp
+    apply (drule_tac x=x and y=y in pd_pts_inj_or_empty, clarsimp+)
+    apply blast
+   apply fastforce
+  apply (rule sym)
+  apply (rule sep_map_set_conj_cong_empty_eq)
+    apply clarsimp+
+  apply (rule box_equals[OF pd_quotient_eq_pts_of_pds[symmetric]], assumption)
+   apply (clarsimp simp: parent_obj_of_def, intro set_eqI iffI;
+          clarsimp simp: quotient_def Image_def)
+    apply (guess_exI, clarsimp)
+    apply (guess_exI, clarsimp)
+    apply (clarsimp simp: cap_ref_object_def)
+    apply (metis (mono_tags, lifting) cap_at_def domI option.sel)
+   apply (guess_exI, clarsimp)
+   apply (guess_exI, clarsimp)
+   apply (clarsimp simp: cap_ref_object_def)
+   apply (metis (mono_tags, lifting) cap_at_def domI option.sel)
+  apply blast
   done
 
-lemma map_map_page_directory_page_tables_wp'':
-  "\<lbrace>\<guillemotleft>(\<And>* obj_id \<in> {obj_id. pt_at obj_id spec \<and>
-                           (\<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and>
-                                  obj_id = cap_object cap)}.
-         object_empty spec t obj_id) \<and>*
-      (\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}. object_initialised spec t obj_id) \<and>*
-      si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-      si_objects \<and>* R\<guillemotright> and
-    K (well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
-   mapM_x (map_page_directory_page_tables spec orig_caps)
-          [obj\<leftarrow>obj_ids . pd_at obj spec]
-   \<lbrace>\<lambda>_. \<guillemotleft>(\<And>* obj_id \<in> {obj_id. pt_at obj_id spec \<and>
-                           (\<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and>
-                                  obj_id = cap_object cap)}.
-         object_initialised spec t obj_id) \<and>*
-         (\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}. object_initialised spec t obj_id) \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm, clarsimp)
-  apply (subst fake_pt_cap_rewrite, assumption)+
-  apply (subst fake_pt_cap_at_conversion [symmetric], assumption)+
-  apply simp
-  apply (rule mapM_x_set_sep'[where
-              I = "(\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}.
-                        object_initialised spec t obj_id) \<and>*
-                   si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>* si_objects",
-              unfolded sep_conj_assoc,simplified])
-    apply simp
-   apply simp
-  apply simp
-  apply (wp sep_wp: map_page_directory_page_tables_wp [where t=t])
-  apply simp
-  apply (subst (asm) sep.prod.remove, simp, simp)
-  apply (subst sep.prod.remove, simp, simp)
-  apply clarsimp
-  apply sep_solve
-  done
-
-lemma map_map_page_directory_page_tables_wp:
-  "\<lbrace>\<guillemotleft>(\<And>* obj_id \<in> {obj_id. pt_at obj_id spec}. object_empty spec t obj_id) \<and>*
-     (\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}. object_initialised spec t obj_id) \<and>*
-     si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and
-     K(well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
-   mapM_x (map_page_directory_page_tables spec orig_caps)
-          [obj\<leftarrow>obj_ids. pd_at obj spec]
-   \<lbrace>\<lambda>_. \<guillemotleft>(\<And>* obj_id \<in> {obj_id. pt_at obj_id spec}. object_initialised spec t obj_id) \<and>*
-         (\<And>* obj_id \<in> {obj_id. pd_at obj_id spec}. object_initialised spec t obj_id) \<and>*
-         si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
-  apply (rule hoare_gen_asm, clarsimp)
-  apply (subst sep_map_set_conj_restrict [where xs="{obj_id. pt_at obj_id spec}" and
-         t="\<lambda>obj_id. \<exists>cap. cap \<in> all_caps spec \<and> is_fake_pt_cap cap \<and> obj_id = cap_object cap"], simp)+
-  apply (clarsimp simp: sep_conj_assoc)
-  apply (subst map_object_empty_initialised_pt, assumption)
-  apply (wp sep_wp: map_map_page_directory_page_tables_wp'' [where t=t], simp+)
-  apply sep_solve
+lemma pt_parents_pd_pts_init:
+  "well_formed spec \<Longrightarrow>
+   (SETSEPCONJ pd_id | pd_at pd_id spec.
+        slots_in_object_init (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec) pd_id spec t) =
+   (SETSEPCONJ pt_id | pt_at pt_id spec \<and> (\<exists>obj. pd_at obj spec \<and> parent_obj_of obj pt_id spec).
+        object_initialised spec t pt_id)"
+  apply (rule sym, subst sep_map_set_quotient_split[where R="pd_equiv_class spec"])
+    apply (clarsimp)
+   apply (rule equivI; clarsimp simp: pd_equiv_sym[simplified fun_app_def] pd_equiv_trans)
+  apply (clarsimp simp: slots_in_object_init_def, rule sym, subst sep_map_set_squash)
+    apply clarsimp
+    apply (drule_tac x=x and y=y in pd_pts_inj_or_empty, clarsimp+)
+    apply blast
+   apply clarsimp
+  apply (rule sym)
+  apply (rule sep_map_set_conj_cong_empty_eq)
+    apply clarsimp+
+  apply (rule box_equals [OF pd_quotient_eq_pts_of_pds[symmetric]], assumption)
+   apply (clarsimp simp: parent_obj_of_def, intro set_eqI iffI;
+          clarsimp simp: quotient_def Image_def)
+    apply (guess_exI, clarsimp)
+    apply (guess_exI, clarsimp)
+    apply (clarsimp simp: cap_ref_object_def)
+    apply (metis (mono_tags, lifting) cap_at_def domI option.sel)
+   apply (guess_exI, clarsimp)
+   apply (guess_exI, clarsimp)
+   apply (clarsimp simp: cap_ref_object_def)
+   apply (metis (mono_tags, lifting) cap_at_def domI option.sel)
+  apply blast
   done
 
 lemma init_vspace_sep:
-  "\<lbrace>\<guillemotleft>objects_empty spec t {obj_id. table_at obj_id spec} \<and>*
+  "\<lbrace>\<guillemotleft>si_objects \<and>*
      si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-     si_objects \<and>* R\<guillemotright> and
-     K(well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace>
-   init_vspace spec orig_caps obj_ids
-   \<lbrace>\<lambda>_. \<guillemotleft>objects_initialised spec t {obj_id. table_at obj_id spec} \<and>*
+     objects_empty spec t {obj_id. table_at obj_id spec} \<and>*
+     (SETSEPCONJ x | pd_at x spec.
+        frame_duplicates_empty (make_frame_cap_map obj_ids free_cptrs spec) x spec) \<and>*
+     R\<guillemotright> and K (
+      well_formed spec \<and>
+      set obj_ids = dom (cdl_objects spec) \<and>
+      distinct obj_ids \<and>
+      card (\<Union> (set ` get_frame_caps spec ` {obj. pd_at obj spec})) \<le> length free_cptrs \<and>
+      list_all (\<lambda>n. n < 2 ^ si_cnode_size) free_cptrs \<and>
+      (\<forall>p. p \<in> {obj_id. pd_at obj_id spec} \<longrightarrow> the (orig_caps p) < 2 ^ si_cnode_size))\<rbrace>
+   init_vspace spec orig_caps obj_ids free_cptrs
+   \<lbrace>\<lambda>_. \<guillemotleft>si_objects \<and>*
          si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
-         si_objects \<and>* R\<guillemotright>\<rbrace>"
+         objects_initialised spec t {obj_id. table_at obj_id spec} \<and>*
+         (SETSEPCONJ x | pd_at x spec.
+            frame_duplicates_copied (make_frame_cap_map obj_ids free_cptrs spec) x spec t) \<and>*
+         R\<guillemotright>\<rbrace>"
   apply (rule hoare_gen_asm, clarsimp)
   apply (clarsimp simp: objects_empty_def objects_initialised_def)
   apply (subst sep_map_set_conj_set_disjoint, simp+,
          clarsimp simp: object_at_def object_type_is_object)+
   apply (clarsimp simp: init_vspace_def sep_conj_assoc)
-  apply (wp sep_wp: map_map_page_directory_page_tables_wp [where t=t]
-                    map_map_page_directory_wp [where t=t], simp+)
-  apply (sep_solve)
-  done
+  apply (wp sep_hoare_fold_mapM_x[OF map_page_directory_wp[simplified sep_wp_simp]], simp+)
+     apply (frule_tac obj_id=x in well_formed_pd_slots; clarsimp)
+     using Ball_set apply fastforce
+    apply (clarsimp simp: make_frame_cap_map_def si_cnode_size_def split: option.splits)
+    apply (meson list_all_spec map_of_SomeD set_zip_rightD)
+   apply (fastforce elim: list_all_spec)
+  apply sep_flatten
+  apply sep_fold_cancel
+  apply (rule sep_map_set_sep_foldI)
+   apply (clarsimp simp: sep.prod.distrib)+
+  apply sep_cancel+
+    (* Split PTs into those which have a parent and those which do not *)
+  apply (clarsimp simp: sep_map_set_conj_restrict
+                          [where t="\<lambda>pt_id. (\<exists>obj. pd_at obj spec \<and> parent_obj_of obj pt_id spec)"
+                             and xs="{obj_id. pt_at obj_id spec}"])
+  apply (clarsimp simp: pt_parents_pd_pts_empty pt_parents_pd_pts_init, sep_cancel+)
+  apply (subst (asm) sep_map_set_conj_subst[OF well_formed_pt_not_in_pd_empty_init])
+     apply fastforce+
+   apply (clarsimp simp: parent_obj_of_def)
+   apply (erule_tac x=obj in allE, drule mp, assumption, clarsimp simp: cap_at_def)
+   apply (fastforce simp: cap_ref_object_def)
+  by sep_solve
 
 lemma init_pd_asids_sep:
   "\<lbrace>\<guillemotleft>si_caps_at t orig_caps spec False {obj_id. real_object_at obj_id spec} \<and>*
@@ -1167,7 +1186,6 @@ lemma init_pd_asids_sep:
   apply (rule mapM_x_wp', clarsimp)
   apply (wp sep_wp: set_asid_wp [where t=t], simp+, sep_solve)
   done
-
 end
 
 end
diff --git a/sys-init/Mapped_Separating_Conjunction.thy b/sys-init/Mapped_Separating_Conjunction.thy
new file mode 100644
index 000000000..f9aff3d1b
--- /dev/null
+++ b/sys-init/Mapped_Separating_Conjunction.thy
@@ -0,0 +1,216 @@
+(*
+ * Copyright 2019, Data61
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ *)
+
+(* Utility lemmas related to the mapping of separating conjunctions over sets and lists *)
+
+theory Mapped_Separating_Conjunction
+imports
+  Sep_Algebra.Sep_Algebra_L4v
+  "HOL-Library.Multiset"
+begin
+
+lemmas sep_map_set_conj_set_cong = arg_cong[where f="sep_map_set_conj P" for P]
+
+lemma sep_map_set_conj_set_elim:
+  "sep_map_set_conj P xs s \<Longrightarrow> \<lbrakk> \<And>x s. x \<in> xs \<Longrightarrow> P x s = Q x s\<rbrakk> \<Longrightarrow>  sep_map_set_conj Q xs s"
+  apply (induct xs arbitrary: s rule: infinite_finite_induct)
+    apply fastforce
+   apply fastforce
+  apply clarsimp
+  apply (erule sep_conj_impl; blast)
+  done
+
+lemma split_filter_set: "xs = {x \<in> xs. P x} \<union> {x \<in> xs. \<not>P x}"
+  by blast
+
+lemma set_minus_not_filter[simp]: "{x \<in> xs. P x} - {x \<in> xs. \<not>P x} = {x \<in> xs. P x}"
+  by blast
+
+lemma set_minus_not_filter'[simp]: "{x \<in> xs. \<not>P x} - {x \<in> xs. P x} = {x \<in> xs. \<not>P x}"
+  by blast
+
+lemma set_inter_not_filter[simp]: "{x \<in> xs. P x} \<inter> {x \<in> xs. \<not>P x} = {}"
+  by blast
+
+declare sep_list_conj_map_add[simp]
+
+lemma sep_map_list_conj_decomp[simp]:
+  "sep_map_list_conj (\<lambda>(x, y). P x y \<and>* Q x y) xs =
+     (sep_map_list_conj (\<lambda>(x, y). P x y) xs \<and>* sep_map_list_conj (\<lambda>(x , y). Q x y) xs)"
+  apply (intro ext iffI)
+   apply (induct xs; clarsimp)
+   apply sep_cancel+
+   apply fastforce
+  apply (induct xs; clarsimp)
+  apply sep_cancel+
+  apply fastforce
+  done
+
+lemma image_insertD: "insert (P x) (P ` S) = Q ` S' \<Longrightarrow> \<exists>s\<in>S'. Q s = P x "
+  by (metis imageE insertI1)
+
+lemma sep_map_set_inj_eqI:
+  "inj_on P xs \<Longrightarrow> inj_on Q ys \<Longrightarrow> P ` xs = Q ` ys \<Longrightarrow>
+   sep_map_set_conj P xs = sep_map_set_conj Q ys"
+  apply (induct xs arbitrary: ys rule: infinite_finite_induct)
+    apply clarsimp
+    defer
+    apply clarsimp+
+   apply (frule image_insertD)
+   apply clarsimp
+   apply atomize
+   apply (erule_tac x="ys - {s}" in allE)
+   apply (drule mp)
+    apply (simp add: inj_on_diff)
+   apply (drule mp)
+    apply (metis (no_types, hide_lams) image_insert inj_on_insert insert_Diff_single
+                                       insert_absorb insert_ident)
+   apply clarsimp
+   apply (subgoal_tac "finite ys")
+    apply (simp add: sep.prod.remove)
+   apply (metis finite.insertI finite_image_iff)
+  apply (subgoal_tac "infinite ys", clarsimp)
+  using finite_image_iff by fastforce
+
+lemma add_mset_eq_mem:
+  "add_mset (P x) (image_mset P (mset_set F)) = image_mset Q (mset_set S')
+   \<Longrightarrow> \<exists>y. Q y = P x \<and> y \<in> S'"
+  apply (drule union_single_eq_member)
+  apply clarsimp
+  by (metis elem_mset_set empty_iff infinite_set_mset_mset_set)
+
+lemma sep_map_set_conj_mset_eq:
+  "\<lbrakk>image_mset P (mset_set S) = image_mset Q (mset_set S');
+    finite S; finite S'\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj P S = sep_map_set_conj Q S'"
+  apply (induction S arbitrary: S' rule: infinite_finite_induct; clarsimp)
+   apply (simp add: mset_set_empty_iff)
+  apply (subgoal_tac "\<exists>y. y \<in> S' \<and> Q y = P x")
+   apply (clarsimp simp: sep.prod.remove mset_set.remove)
+  by (fastforce dest: union_single_eq_member)
+
+lemma sep_map_set_conj_multisetE:
+  "\<lbrakk>sep_map_set_conj P S s; finite S; finite S';
+    image_mset P (mset_set S) = image_mset Q (mset_set S')\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj Q S' s"
+  by (subst sep_map_set_conj_mset_eq; fastforce)
+
+lemma not_in_image_vimage: "x \<notin> P ` S \<Longrightarrow> P -` {x} \<inter> S = {}"
+  by blast
+
+lemma bij_image_mset_eq:
+  "\<lbrakk>finite S; finite S'; P ` S = Q ` S';
+    (\<And>x. x \<in> P ` S \<Longrightarrow> \<exists>f. bij_betw f (P -` {x} \<inter> S) (Q -` {x} \<inter> S'))\<rbrakk>
+   \<Longrightarrow> image_mset P (mset_set S) = image_mset Q (mset_set S')"
+  apply (rule multiset_eqI)
+  apply (clarsimp simp: count_image_mset)
+  apply (case_tac "x \<in> Q ` S'"; clarsimp simp: bij_betw_iff_card not_in_image_vimage )
+  done
+
+lemma sep_map_set_elim:
+  "\<lbrakk>sep_map_set_conj P xs s;
+    xs = ys;
+    (\<And>x s. x \<in> xs \<Longrightarrow> P x s \<Longrightarrow> Q x s)\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj Q ys s"
+  apply clarsimp
+  apply (case_tac "finite xs")
+   apply clarsimp
+   apply (erule sep_map_set_conj_impl)
+    apply atomize
+    apply (erule_tac x=x in allE)
+    apply clarsimp
+   apply clarsimp
+  apply clarsimp
+  done
+
+lemma sep_map_set_conj_Union:
+  "\<lbrakk>\<forall>s \<in> S. finite s;
+    \<forall>s s'. s \<in> S \<and> s' \<in> S \<longrightarrow> s \<noteq> s' \<longrightarrow> s \<inter> s' = {}\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) S = sep_map_set_conj P (\<Union> S) "
+  apply (induct S rule: infinite_finite_induct; clarsimp)
+   apply (metis (no_types) finite_UnionD sep.prod.infinite)
+  apply (subst sep.prod.union_disjoint; clarsimp?)
+  by blast
+
+lemma sep_map_set_quotient_split:
+  "\<lbrakk>finite xs; equiv xs R\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj P xs = sep_map_set_conj (sep_map_set_conj P ) (xs//R) "
+  apply (subst sep_map_set_conj_Union; clarsimp)
+    apply (meson in_quotient_imp_subset infinite_super)
+   apply (fastforce dest: quotient_disj)
+  by (simp add: Union_quotient)
+
+lemma sep_map_set_conj_congE:
+  "\<lbrakk>sep_map_set_conj (sep_map_set_conj P) xs s;
+    finite xs;
+    finite ys;
+    xs - {{}} = ys - {{}}\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) ys s"
+  apply clarsimp
+  apply (induct xs arbitrary:ys s rule: infinite_finite_induct)
+    apply clarsimp+
+   apply (subgoal_tac "ys = {{}} \<or> ys = {}")
+    apply (erule disjE; clarsimp)
+   apply blast
+  apply clarsimp
+  apply (case_tac "x = {}")
+   apply (metis Diff_idemp Diff_insert_absorb Sep_Tactic_Helpers.sep_conj_empty sep.prod.empty)
+  apply (subgoal_tac "x \<in> ys")
+   apply (clarsimp simp: sep.prod.remove)
+   apply sep_cancel
+   apply (metis Diff_insert Diff_insert2 Diff_insert_absorb finite_Diff)
+  apply blast
+  done
+
+lemma sep_map_set_conj_cong_empty_eq:
+  "\<lbrakk>finite xs;
+    finite ys;
+    xs - {{}} = ys - {{}}\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj (sep_map_set_conj P) xs = sep_map_set_conj (sep_map_set_conj P) ys "
+  apply clarsimp
+  apply (intro ext iffI; erule sep_map_set_conj_congE)
+  by blast+
+
+lemma sep_map_set_conj_match:
+  "sep_map_set_conj P S s \<Longrightarrow> (\<And>x s. x \<in> S \<Longrightarrow> P x s \<Longrightarrow> Q x s) \<Longrightarrow> sep_map_set_conj Q S s"
+  apply (induct rule: infinite_finite_induct; clarsimp)
+  apply (erule sep_conj_impl)
+   apply blast
+  by (metis sep_map_set_elim)
+
+lemma sep_map_set_squash:
+  "\<lbrakk>\<forall>x y. x \<in> S \<longrightarrow> y \<in> S \<longrightarrow> x \<noteq> y \<longrightarrow> f x = f y \<longrightarrow> f x = {}; finite S\<rbrakk>
+   \<Longrightarrow> sep_map_set_conj (\<lambda>v. sep_map_set_conj P (f v)) S =
+      sep_map_set_conj (sep_map_set_conj P) (f ` S)"
+  apply (induction S rule: infinite_finite_induct; clarsimp)
+  apply (case_tac "f x \<in> f ` F"; clarsimp)
+  apply (subgoal_tac "f x = {}")
+   apply clarsimp
+  apply blast
+  done
+
+lemma sep_map_set_conj_subst:
+  "(\<And>x. x \<in> S \<Longrightarrow> Q x = Q' x) \<Longrightarrow> sep_map_set_conj Q S = sep_map_set_conj Q' S"
+  by clarsimp
+
+lemma sep_map_zip_fst:
+  "(\<And>* map (\<lambda>(a,b). f a) (zip xs ys)) s =
+   (\<And>* map (\<lambda>a. f (fst a)) (zip xs ys)) s"
+  by (simp add: case_prod_unfold)
+
+lemma sep_map_zip_snd:
+  "(\<And>* map (\<lambda>(a, b). f b) (zip xs ys)) s =
+   (\<And>* map (\<lambda>a. f (snd a)) (zip xs ys)) s"
+  by (simp add: case_prod_unfold)
+
+declare sep_map_zip_fst[THEN iffD1, sep_cancel] sep_map_zip_fst[THEN iffD2, sep_cancel]
+        sep_map_zip_snd[THEN iffD1, sep_cancel] sep_map_zip_snd[THEN iffD2, sep_cancel]
+
+end
diff --git a/sys-init/ObjectInitialised_SI.thy b/sys-init/ObjectInitialised_SI.thy
index 4d898e073..30f88b15c 100644
--- a/sys-init/ObjectInitialised_SI.thy
+++ b/sys-init/ObjectInitialised_SI.thy
@@ -146,6 +146,23 @@ where
   "object_empty_slots_empty spec t spec_object_id \<equiv>
   object_initialised_general spec t object_default_state sep_map_E spec_object_id"
 
+definition slots_in_object_empty ::
+  "(cdl_cap \<Rightarrow> bool) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow>
+   (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> sep_pred" where
+  "slots_in_object_empty P obj_id spec t \<equiv>
+     sep_map_set_conj (object_empty spec t)
+                      {obj. \<exists>slot. slot \<in> dom (slots_of obj_id spec)
+                                   \<and> cap_at P (obj_id, slot) spec
+                                   \<and> obj = cap_ref_object (obj_id, slot) spec}"
+
+definition slots_in_object_init ::
+  "(cdl_cap \<Rightarrow> bool) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow>
+   (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> sep_pred" where
+  "slots_in_object_init P obj_id spec t \<equiv>
+     sep_map_set_conj (object_initialised spec t)
+                      {obj. \<exists>slot. slot \<in> dom (slots_of obj_id spec)
+                                   \<and> cap_at P (obj_id, slot) spec
+                                   \<and> obj = cap_ref_object (obj_id, slot) spec}"
 
 (**********************************************
  * Predicates about CNodes being initialised. *
@@ -436,6 +453,16 @@ lemma cap_transform_nullcap [simp]:
   by (clarsimp simp: cap_transform_def cap_has_object_def
                      update_cap_object_def)
 
+lemma cap_transform_pt_simp [simp]:
+  "cap_transform t (PageTableCap x y z) = PageTableCap (the (t x)) y z"
+  by (clarsimp simp: option.the_def cap_transform_def update_cap_object_def cap_object_def
+               split: option.splits)
+
+lemma cap_transform_frame [simp]:
+  "cap_transform t (FrameCap x ptr rights n y z) = FrameCap x (the (t ptr)) rights n y z"
+  by (clarsimp simp: option.the_def cap_transform_def update_cap_object_def cap_object_def
+               split: option.splits)
+
 lemma cap_type_cap_transform [simp]:
   "cap_type (cap_transform t cap) = cap_type cap"
   by (clarsimp simp: cap_transform_def cap_has_object_def)
@@ -1375,4 +1402,10 @@ lemma object_fields_empty_half_initialised:
   \<Longrightarrow> cnode_fields_half_initialised spec t obj_id = object_fields_empty spec t obj_id"
   by (clarsimp simp: cnode_fields_half_initialised_object_fields_initialised cnode_fields_empty_initialised)
 
+lemma object_default_state_frame [simp]:
+  "is_frame object \<Longrightarrow> object_default_state object = object"
+  by (clarsimp simp: object_default_state_def default_object_def
+                     object_type_is_object object_type_def
+              split: cdl_object.splits)
+
 end
diff --git a/sys-init/Proof_SI.thy b/sys-init/Proof_SI.thy
index dd156455d..6b4529ff4 100644
--- a/sys-init/Proof_SI.thy
+++ b/sys-init/Proof_SI.thy
@@ -47,24 +47,6 @@ lemma parse_bootinfo_sep:
   apply (clarsimp simp: zip_map1 comp_def split_beta')
   done
 
-lemma parse_spec_inv:
-  "\<lbrace>\<lambda>s. \<guillemotleft>R\<guillemotright> s\<rbrace>
-     parse_spec spec obj_ids
-   \<lbrace>\<lambda>rv s. \<guillemotleft>R\<guillemotright> s\<rbrace>"
-  apply (clarsimp simp: parse_spec_def sep_state_projection2_def)
-  apply (wp)
-  apply clarsimp
-  done
-
-lemma parse_spec_sep:
-  "\<lbrace>\<lambda>s. True\<rbrace>
-     parse_spec spec obj_ids
-   \<lbrace>\<lambda>_ s. set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids \<rbrace>"
-  apply (clarsimp simp: parse_spec_def)
-  apply (wp)
-  apply clarsimp
-  done
-
 (* This isn't actually all the combinations, but enough of them for what I needed. *)
 lemma object_types_distinct:
  "tcb_at x s     \<Longrightarrow> \<not> cnode_at x s"
@@ -100,13 +82,6 @@ lemma real_objects_some_type:
                  split: cdl_object.splits)
   by metis
 
-lemma object_at_irq_node_irq_node_at:
-  "\<lbrakk>well_formed spec; object_at P obj_id spec; obj_id \<in> irq_nodes spec\<rbrakk> \<Longrightarrow> irq_node_at obj_id spec"
-  apply (clarsimp simp: object_at_def)
-  apply (frule (2) well_formed_irq_nodes_object_type)
-  apply (simp add: object_type_is_object)
-  done
-
 lemma capdl_objects_by_parts:
   "well_formed spec \<Longrightarrow>
    (sep_map_set_conj P {obj_id. real_object_at obj_id spec}) =
@@ -168,16 +143,12 @@ lemma valid_case_prod':
 
 lemma le_list_all:
   "\<lbrakk>unat start < 2 ^ si_cnode_size; unat (end - 1) < 2 ^ si_cnode_size\<rbrakk>
-  \<Longrightarrow> list_all (\<lambda>n. (n::32 word) < 2 ^ si_cnode_size) [start .e. end - 1]"
+   \<Longrightarrow> list_all (\<lambda>n. (n::32 word) < 2 ^ si_cnode_size) [start .e. end - 1]"
   apply (clarsimp simp: list_all_iff)
   apply (subst word_arith_power_alt)
   apply simp
   by (metis (no_types) dual_order.strict_trans2 unat_less_2_si_cnode_size word_of_int_numeral word_of_int_power_hom)
 
-lemma sep_conj_pred_conj:
-  "(P \<and>* (P' and K Q)) s = ((P \<and>* P') and K Q) s"
-  by (case_tac "Q = False", simp_all)
-
 lemma list_all_drop:
   "list_all P xs \<Longrightarrow> list_all P (drop n xs)"
   by (fastforce simp: list_all_iff dest: in_set_dropD)
@@ -188,6 +159,23 @@ lemma dom_map_of_zip':
   apply (subst dom_map_of_zip, simp+)
   done
 
+(* FIXME: MOVE (Lib) *)
+lemma in_zip_map: "p \<in> set xs \<Longrightarrow> length xs \<le> length ys \<Longrightarrow> map_of (zip xs ys) p \<noteq> None"
+  using dom_map_of_zip' by blast
+
+lemma map_of_list_allE:
+  "map_of (zip ys xs) p = Some v \<Longrightarrow> distinct ys \<Longrightarrow> list_all P xs \<Longrightarrow> P v"
+  apply (induct ys arbitrary: xs; clarsimp)
+  by (meson in_set_zipE list_all_spec map_of_SomeD)
+
+lemma card_eq_lengthI:
+  "set xs = ys \<Longrightarrow> distinct xs \<Longrightarrow> length xs = card ys"
+  by (induct xs arbitrary: ys; fastforce)
+
+lemma length_filter_card:
+  "\<lbrakk>s_list = sorted_list_of_set s; finite s\<rbrakk>
+   \<Longrightarrow> length (filter P s_list) = card {x \<in> s. P x}"
+  by (fastforce intro: card_eq_lengthI)
 
 (* Dirty hack that is sadly needed to make the below proof work. *)
 declare [[unify_search_bound = 1000]]
@@ -196,7 +184,8 @@ lemma small_one:
   "\<lbrakk>well_formed spec;
    set obj_ids = dom (cdl_objects spec); distinct obj_ids;
    real_ids = [obj_id \<leftarrow> obj_ids. real_object_at obj_id spec];
-   length obj_ids + length [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] \<le> unat fend - unat fstart;
+   length obj_ids + length [obj\<leftarrow>obj_ids. cnode_or_tcb_at obj spec] +
+   card (\<Union>(set ` get_frame_caps spec ` {obj. pd_at obj spec})) \<le> unat fend - unat fstart;
    length untyped_caps = unat uend - unat ustart;
    distinct_sets (map cap_free_ids untyped_caps);
    list_all is_full_untyped_cap untyped_caps;
@@ -216,7 +205,12 @@ lemma small_one:
    \<lbrace>\<guillemotleft>(\<And>* (cptr, cap) \<in> set (zip untyped_cptrs untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap) \<and>*
      (\<And>* cptr \<in> set free_cptrs. (si_cnode_id, unat cptr) \<mapsto>c NullCap)  \<and>*
      (\<And>* obj_id\<in>(\<Union>cap\<in>set untyped_caps. cap_free_ids cap). obj_id \<mapsto>o Untyped) \<and>*
-    si_objects \<and>* si_irq_nodes spec \<and>* R\<guillemotright>\<rbrace>
+    si_objects \<and>*
+    si_irq_nodes spec \<and>*
+    (SETSEPCONJ pd_id | pd_at pd_id spec.
+      frame_duplicates_empty (make_frame_cap_map obj_ids (drop (length obj_ids) free_cptrs) spec)
+                             pd_id spec) \<and>*
+    R\<guillemotright>\<rbrace>
    init_system spec bootinfo obj_ids
   \<lbrace>\<lambda>_ s. \<exists>t.
     \<guillemotleft>objects_initialised spec t {obj_id. real_object_at obj_id spec} \<and>*
@@ -226,8 +220,12 @@ lemma small_one:
      si_objects \<and>*
      si_objects_extra_caps (dom (cdl_objects spec))
                             (free_cptrs :: 32 word list)
-                            (untyped_cptrs :: 32 word list) spec \<and>* R\<guillemotright> s \<and>
-     inj_on t (dom (cdl_objects spec)) \<and> dom t = set obj_ids\<rbrace>"
+                            (untyped_cptrs :: 32 word list) spec \<and>*
+    (SETSEPCONJ pd_id | pd_at pd_id spec.
+      frame_duplicates_copied (make_frame_cap_map obj_ids (drop (length obj_ids) free_cptrs) spec)
+                              pd_id spec t) \<and>*
+    R\<guillemotright> s \<and>
+    inj_on t (dom (cdl_objects spec)) \<and> dom t = set obj_ids\<rbrace>"
   apply clarsimp
   apply (frule (1) le_list_all [where start = ustart])
   apply (frule (1) le_list_all [where start = fstart])
@@ -235,73 +233,74 @@ lemma small_one:
   apply (insert distinct_card [symmetric, where xs ="[obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec]"], simp)
   apply (frule distinct_card [symmetric])
   apply (clarsimp simp: init_system_def, wp valid_case_prod')
-           apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in start_threads_sep [sep_wandise], simp)
-          apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and
-                                                 free_cptrs="[fstart .e. fend - 1]" in init_cspace_sep [sep_wandise])
-         apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_tcbs_sep [sep_wandise])
-        apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_vspace_sep [sep_wandise])
-       apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_pd_asids_sep [sep_wandise])
-      apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False in init_irqs_sep [sep_wandise])
-     apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False and
-                                            untyped_cptrs = "[ustart .e. uend - 1]" and
-                                            free_cptrs_orig = "[fstart .e. fend - 1]" in duplicate_caps_sep [sep_wandise])
+            apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in start_threads_sep [sep_wandise], simp)
+           apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and
+                                                  free_cptrs="[fstart .e. fend - 1]" in init_cspace_sep [sep_wandise])
+          apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_tcbs_sep [sep_wandise])
+         apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_vspace_sep [sep_wandise])
+        apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t in init_pd_asids_sep [sep_wandise])
+       apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False in init_irqs_sep [sep_wandise])
+      apply (rule hoare_ex_wp, rename_tac t, rule_tac t=t and dev=False and
+                                             untyped_cptrs = "[ustart .e. uend - 1]" and
+                                             free_cptrs_orig = "[fstart .e. fend - 1]" in duplicate_caps_sep [sep_wandise])
      apply (rule create_irq_caps_sep [where dev = False,sep_wandise,
             where free_cptrs_orig = "[fstart .e. fend - 1]"
               and untyped_cptrs = "[ustart .e. uend - 1]"
-              and orig_caps = "map_of (zip [obj\<leftarrow>obj_ids. real_object_at obj spec] [fstart .e. fend - 1])"
+              and orig_caps = "map_of (zip [obj\<leftarrow>obj_ids. real_object_at obj spec]
+                                           [fstart .e. fend - 1])"
               and spec = spec])
     apply (wp sep_wp: create_objects_sep [where untyped_caps = untyped_caps and dev = False])
-    apply (wp sep_wp: parse_bootinfo_sep [where fstart = fstart
-                                            and fend = fend
-                                            and ustart = ustart
-                                            and uend = uend
-                                            and untyped_caps = untyped_caps])
+   apply (wp sep_wp: parse_bootinfo_sep [where fstart = fstart
+                                           and fend = fend
+                                           and ustart = ustart
+                                           and uend = uend
+                                           and untyped_caps = untyped_caps])
   apply (subst objects_initialised_by_parts, assumption)
   apply (subst objects_empty_by_parts, assumption)+
   apply (subst objects_empty_objects_initialised_capless)+
-  apply clarsimp
-  apply (sep_cancel+ | intro conjI allI impI | erule sep_curry[rotated, where P=R])+
-  apply simp
-  apply (intro conjI allI impI | sep_cancel+)+
-   apply (intro conjI pred_andI)
-      apply sep_cancel+
-      apply (intro conjI pred_andI allI impI)
-      apply (erule sep_curry[rotated, where P=R])
-      apply (intro conjI pred_andI allI impI)
-       apply sep_solve
+  apply (clarsimp simp: linorder_not_le)
+  apply (intro conjI allI impI pred_andI | sep_cancel+)+
+         apply fastforce
+        apply (clarsimp simp: less_diff_conv)
+        apply (rule list_all_drop, erule (1) le_list_all)
+       apply clarsimp
+       apply (subgoal_tac "map_of (zip (filter (\<lambda>obj. real_object_at obj spec) obj_ids) free_cptrs)
+                                  p \<noteq> None")
+        apply clarsimp
+        apply (erule map_of_list_allE)
+         apply (fastforce intro!: List.distinct_filter)
+        apply (fastforce intro!: le_list_all)
+       apply (rule in_zip_map)
+        apply clarsimp
+        apply (fastforce dest!: real_object_not_irq_node(3))
+       apply (insert length_filter_le[where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"],
+              fastforce)[1]
       apply (erule (1) le_list_all)
      apply (rule list_all_drop, erule (1) le_list_all)
     apply simp
    apply (subst dom_map_of_zip')
-    apply (insert length_filter_le [where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"], simp)
+    apply (insert length_filter_le [where xs = obj_ids and P="\<lambda>obj. real_object_at obj spec"],
+           fastforce)[1]
    apply simp
   apply (erule (1) le_list_all)
   done
 
-(* FIXME, make the acquiring of the object_ids part of sys_init, not a parameter. *)
-
-
-
-lemma set_inter_rewrite:
-  " ({x. P x} \<inter> S) =
-     {x \<in> S. P x}"
-  by fast
-
-
 (**************************************************
  * The top level lemma for system initialisation. *
  **************************************************)
+(* FIXME, make the acquiring of the object_ids part of sys_init, not a parameter. *)
 
 lemma sys_init:
-  "\<lbrakk>well_formed spec; set obj_ids = dom (cdl_objects spec); distinct obj_ids\<rbrakk> \<Longrightarrow>
+  "\<lbrakk>well_formed spec; obj_ids = sorted_list_of_set (dom (cdl_objects spec))\<rbrakk> \<Longrightarrow>
    \<lbrace>\<guillemotleft>valid_boot_info bootinfo spec \<and>* R\<guillemotright>\<rbrace>
-   init_system spec bootinfo obj_ids
-  \<lbrace>\<lambda>_ s. \<exists>t.
+    init_system spec bootinfo obj_ids
+   \<lbrace>\<lambda>_ s. \<exists>t.
     \<guillemotleft>objects_initialised spec t {obj_id. real_object_at obj_id spec} \<and>*
      irqs_initialised spec t (used_irqs spec) \<and>*
-     si_final_objects spec t \<and>* R\<guillemotright> s \<and>
+     si_final_objects spec t \<and>*
+     (EXS map. (SETSEPCONJ pd_id | pd_at pd_id spec. frame_duplicates_copied map pd_id spec t)) \<and>*
+     R\<guillemotright> s \<and>
      inj_on t (set obj_ids) \<and> dom t = set obj_ids\<rbrace>"
-  apply (frule distinct_card)
   apply (insert distinct_card [where xs = "[obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec]"], simp)
   apply (clarsimp simp: valid_boot_info_def si_final_objects_def
                         sep_conj_exists sep_conj_assoc)
@@ -309,19 +308,22 @@ lemma sys_init:
   apply (rule hoare_ex_pre)+
   apply (rule hoare_grab_asm)+
   apply (rule hoare_chain)
-   apply (rule small_one [where obj_ids=obj_ids and R=R],
-         (assumption|simp add: unat_less_2_si_cnode_size')+)
-
+    apply (rule small_one[where obj_ids="sorted_list_of_set (dom (cdl_objects spec))" and R=R],
+          (assumption|simp add: unat_less_2_si_cnode_size' length_filter_card)+)
+   apply sep_solve
   apply clarsimp
   apply (rule_tac x=t in exI)
   apply (clarsimp)
   apply (clarsimp simp: si_objects_extra_caps_def si_caps_at_def
                         sep_conj_exists sep_conj_assoc)
-  apply (rule_tac x="(map_of (zip [obj\<leftarrow>obj_ids . cnode_or_tcb_at obj spec] (drop (length obj_ids) [fstart .e. fend - 1])))" in exI)
+  apply (rule_tac x="(map_of (zip [obj \<leftarrow> obj_ids. cnode_or_tcb_at obj spec]
+                                  (drop (length obj_ids) [fstart .e. fend - 1])))" in exI)
   apply (rule_tac x="[x .e. xa - 1]" in exI)
   apply (rule_tac x="[fstart .e. fend - 1]" in exI)
   apply (rule_tac x=untyped_capsa in exI)
   apply (rule_tac x=all_available_ids in exI)
+  apply (rule_tac x="make_frame_cap_map obj_ids (drop (card (dom (cdl_objects spec)))
+                                                      [fstart .e. fend - 1]) spec" in exI)
   apply (clarsimp simp: sep_conj_ac)
   done
 
@@ -329,16 +331,18 @@ definition injective :: "('a \<Rightarrow> 'b option) \<Rightarrow> bool"
 where "injective f \<equiv> inj_on f (dom f)"
 
 lemma sys_init_paper:
-  "\<lbrakk>well_formed spec; set obj_ids = dom (cdl_objects spec); distinct obj_ids\<rbrakk> \<Longrightarrow>
+  "\<lbrakk>well_formed spec; obj_ids = sorted_list_of_set (dom (cdl_objects spec))\<rbrakk> \<Longrightarrow>
    \<lbrace>\<guillemotleft>valid_boot_info bootinfo spec \<and>* R\<guillemotright>\<rbrace>
    init_system spec bootinfo obj_ids
-  \<lbrace>\<lambda>_ s. \<exists>\<phi>.
+   \<lbrace>\<lambda>_ s. \<exists>\<phi>.
     \<guillemotleft>objects_initialised spec \<phi> {obj_id. real_object_at obj_id spec} \<and>*
      irqs_initialised spec \<phi> (used_irqs spec) \<and>*
-     si_final_objects spec \<phi> \<and>* R\<guillemotright> s \<and>
+     si_final_objects spec \<phi> \<and>*
+     (EXS map. (SETSEPCONJ pd_id | pd_at pd_id spec. frame_duplicates_copied map pd_id spec \<phi>)) \<and>*
+     R\<guillemotright> s \<and>
      injective \<phi> \<and> dom \<phi> = set obj_ids\<rbrace>"
   apply (rule hoare_strengthen_post)
-  apply (fact sys_init)
+   apply (fact sys_init)
   apply (fastforce simp: injective_def)
   done
 
diff --git a/sys-init/RootTask_SI.thy b/sys-init/RootTask_SI.thy
index 77a012ab8..9bfd2709c 100644
--- a/sys-init/RootTask_SI.thy
+++ b/sys-init/RootTask_SI.thy
@@ -12,7 +12,7 @@
  * The layout of the capability space and other parts of the system-initialiser.
  *)
 theory RootTask_SI
-imports WellFormed_SI
+imports WellFormed_SI SysInit_SI
 begin
 
 (******************************************************************
@@ -506,6 +506,60 @@ lemma valid_si_caps_at_si_cap_at:
     apply (clarsimp simp: sep_conj_ac)+
   done
 
+(*******************************************************
+ * Frames have been duplicated. *
+ *******************************************************)
+
+abbreviation (input)
+  "lookup_obj obj_id slot P s \<equiv> \<exists>cap. opt_cap (obj_id, slot) s = Some cap
+                                      \<and> cap \<noteq> NullCap
+                                      \<and> P (cap_object cap) s"
+abbreviation "get_obj obj_id slot spec \<equiv> (cap_object o the) (opt_cap (obj_id, slot) spec)"
+abbreviation "ref_obj spec obj_id slot \<equiv> cap_ref_object (obj_id, slot) spec"
+abbreviation "real_frame_cap_of dev ptr rights n t \<equiv> FrameCap dev ((the o t) ptr) rights n Real None"
+abbreviation (input) "the_cap spec pt_id pt_slot \<equiv> the (opt_cap (pt_id, pt_slot) spec)"
+
+definition conjure_real_frame_cap ::
+  "cdl_cap \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> cdl_cap"
+  where
+  "conjure_real_frame_cap cap t \<equiv>
+    case cap of FrameCap _ ptr _ n _ _ \<Rightarrow> real_frame_cap_of False ptr vm_read_write n t | _ \<Rightarrow> cap"
+
+definition frame_duplicates_empty ::
+  "(cdl_object_id \<times> nat \<Rightarrow> word32) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state \<Rightarrow> (sep_state \<Rightarrow> bool)"
+  where
+  "frame_duplicates_empty cptr_map pd_id spec \<equiv>
+   sep_map_set_conj
+    (\<lambda>x. let pt_id = get_obj pd_id x spec in
+         sep_map_set_conj (\<lambda>y. (si_cnode_id, unat $ cptr_map (pt_id, y)) \<mapsto>c NullCap)
+         {slot \<in> dom (slots_of pt_id spec). cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
+    {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec)
+                                              (pd_id, slot) spec} \<and>*
+   sep_map_set_conj
+     (\<lambda>x. let frame_id = get_obj pd_id x spec in
+          (si_cnode_id, unat $ cptr_map (pd_id, x)) \<mapsto>c NullCap)
+     {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> frame_at (cap_object cap) spec)
+                                               (pd_id, slot) spec}"
+
+definition frame_duplicates_copied ::
+  "(cdl_object_id \<times> nat \<Rightarrow> word32) \<Rightarrow> cdl_object_id \<Rightarrow> cdl_state
+   \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_object_id option) \<Rightarrow> (sep_state \<Rightarrow> bool)"
+  where
+  "frame_duplicates_copied cptr_map pd_id spec t \<equiv>
+   sep_map_set_conj
+    (\<lambda>x. let pt_id = get_obj pd_id x spec in
+         sep_map_set_conj (\<lambda>y. (si_cnode_id, unat $ cptr_map (pt_id, y)) \<mapsto>c
+                                 conjure_real_frame_cap (the_cap spec pt_id y) t)
+         {slot \<in> dom (slots_of pt_id spec). cap_at ((\<noteq>) NullCap) (pt_id, slot) spec})
+    {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> pt_at (cap_object cap) spec)
+                                              (pd_id, slot) spec} \<and>*
+   sep_map_set_conj
+     (\<lambda>x. let frame_id = get_obj pd_id x spec in
+          (si_cnode_id, unat $ cptr_map (pd_id, x)) \<mapsto>c
+            conjure_real_frame_cap (the_cap spec pd_id x) t)
+     {slot \<in> dom (slots_of pd_id spec). cap_at (\<lambda>cap. cap \<noteq> NullCap \<and> frame_at (cap_object cap) spec)
+                                               (pd_id, slot) spec}"
+
 (**********************************************************
  * The pre and post conditions of the system initialiser. *
  **********************************************************)
@@ -515,13 +569,20 @@ definition
   valid_boot_info
 where
   "valid_boot_info bootinfo spec \<equiv> \<lambda>s.
-  \<exists>untyped_caps fstart fend ustart uend.
+  \<exists>untyped_caps fstart fend ustart uend obj_ids.
   ((\<And>*(cptr, cap) \<in> set (zip [ustart .e. uend - 1] untyped_caps). (si_cnode_id, unat cptr) \<mapsto>c cap)  \<and>*
    (\<And>* cptr \<in> set [fstart .e. fend - 1]. (si_cnode_id, unat cptr) \<mapsto>c NullCap) \<and>*
    (\<And>* obj_id\<in>(\<Union>cap\<in>set untyped_caps. cap_free_ids cap). obj_id \<mapsto>o Untyped) \<and>*
-    si_objects \<and>* si_irq_nodes spec) s \<and>
+   (SETSEPCONJ pd_id | pd_at pd_id spec.
+     frame_duplicates_empty (make_frame_cap_map obj_ids
+                              (drop (card (dom (cdl_objects spec))) [fstart .e. fend - 1]) spec)
+                            pd_id spec) \<and>*
+   si_objects \<and>*
+   si_irq_nodes spec) s \<and>
+   obj_ids = sorted_list_of_set (dom (cdl_objects spec)) \<and>
    card (dom (cdl_objects spec)) +
-   card {obj_id. cnode_or_tcb_at obj_id spec} \<le> unat fend - unat fstart \<and>
+   card {obj_id. cnode_or_tcb_at obj_id spec} +
+   card (\<Union>(set ` get_frame_caps spec ` {obj. pd_at obj spec})) \<le> unat fend - unat fstart \<and>
    length untyped_caps = unat uend - unat ustart \<and>
    distinct_sets (map cap_free_ids untyped_caps) \<and>
    list_all is_full_untyped_cap untyped_caps \<and>
diff --git a/sys-init/SysInit_SI.thy b/sys-init/SysInit_SI.thy
index 9ccd744d2..a6b38c1cd 100644
--- a/sys-init/SysInit_SI.thy
+++ b/sys-init/SysInit_SI.thy
@@ -27,15 +27,6 @@ where
     return (untyped_list, free_slots)
   od"
 
-(* Currently, objects are created in any order.
-   Later versions could create untypes before their children and use the untyped_covers.
-   A refinement will create bigger ones first to remove internal fragmentation. *)
-definition
-  parse_spec :: "cdl_state \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad"
-where
-  "parse_spec spec obj_ids \<equiv>
-     assert (set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)"
-
 (* Create a new object in the next free cnode slot using a given untyped.
    Return whether or not the operation fails. *)
 definition
@@ -185,7 +176,7 @@ definition duplicate_caps :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarro
                                         \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) u_monad"
 where
   "duplicate_caps spec orig_caps obj_ids free_slots \<equiv> do
-    obj_ids' \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_at obj_id spec \<or> tcb_at obj_id spec];
+    obj_ids' \<leftarrow> return [obj_id \<leftarrow> obj_ids. cnode_or_tcb_at obj_id spec];
     assert (length obj_ids' \<le> length free_slots);
     mapM_x (duplicate_cap spec orig_caps) (zip obj_ids' free_slots);
     return $ map_of $ zip obj_ids' free_slots
@@ -266,58 +257,44 @@ where
     mapM_x (set_asid spec orig_caps) pd_ids
   od"
 
-(* Map the right cap into the slot of a page directory or page table. *)
-definition map_page :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
-                             \<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> unit u_monad"
-where
-  "map_page spec orig_caps page_id pd_id rights vaddr \<equiv> do
+(* Map a page into a page table or page directory *)
+definition map_page ::
+  "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
+   \<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> cdl_cptr \<Rightarrow> unit u_monad"
+  where
+  "map_page spec orig_caps page_id pd_id rights vaddr free_cptr \<equiv> do
     cdl_page  \<leftarrow> assert_opt $ opt_object page_id spec;
     sel4_page \<leftarrow> assert_opt $ orig_caps page_id;
     sel4_pd   \<leftarrow> assert_opt $ orig_caps pd_id;
-
     vmattribs \<leftarrow> assert_opt $ opt_vmattribs cdl_page;
-
-    if (pt_at page_id spec) then
-      seL4_PageTable_Map sel4_page sel4_pd vaddr vmattribs
-    else if (frame_at page_id spec) then
-      seL4_Page_Map sel4_page sel4_pd vaddr rights vmattribs
-    else
-      fail;
-     return ()
+    assert (frame_at page_id spec);
+    \<comment> \<open>Copy the frame cap into a new slot for mapping, this enables shared frames\<close>
+    duplicate_cap spec orig_caps (page_id, free_cptr);
+    seL4_Page_Map free_cptr sel4_pd vaddr rights vmattribs;
+    return ()
   od"
 
-(* Maps a page directory slot (and all its contents if it's a page table). *)
-definition map_page_directory_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
-                                    \<Rightarrow> cdl_object_id\<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
-where
-  "map_page_directory_slot spec orig_caps pd_id pd_slot \<equiv> do
-    page_cap    \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec;
-    page_id     \<leftarrow> return $ cap_object page_cap;
-
-    (* The page table's virtual address is given by the number of slots and how much memory each maps.
-       Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *)
-    page_vaddr  \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size);
-    page_rights \<leftarrow> return (cap_rights page_cap);
-
-    when (page_cap \<noteq> NullCap)
-         (map_page spec orig_caps page_id pd_id page_rights page_vaddr)
-
+(* Map a page table into a page directory *)
+definition map_page_table ::
+  "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
+   \<Rightarrow> cdl_object_id \<Rightarrow> cdl_right set \<Rightarrow> word32 \<Rightarrow> unit u_monad"
+  where
+  "map_page_table spec orig_caps page_id pd_id rights vaddr \<equiv> do
+    cdl_page  \<leftarrow> assert_opt $ opt_object page_id spec;
+    sel4_page \<leftarrow> assert_opt $ orig_caps page_id;
+    sel4_pd   \<leftarrow> assert_opt $ orig_caps pd_id;
+    vmattribs \<leftarrow> assert_opt $ opt_vmattribs cdl_page;
+    assert (pt_at page_id spec);
+    seL4_PageTable_Map sel4_page sel4_pd vaddr vmattribs;
+    return ()
   od"
 
-(* Maps a page directory and all its contents. *)
-definition map_page_directory :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
-                                                                                   \<Rightarrow> unit u_monad"
-where
-  "map_page_directory spec orig_caps pd_id \<equiv> do
-    pd_slots \<leftarrow> return $ slots_of_list spec pd_id;
-    mapM_x (map_page_directory_slot spec orig_caps pd_id) pd_slots
-  od"
-
-(* Maps a page directory slot. *)
-definition map_page_table_slot :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
-                                      \<Rightarrow> cdl_object_id \<Rightarrow> word32 \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
-where
-  "map_page_table_slot spec orig_caps pd_id pt_id pt_vaddr pt_slot \<equiv> do
+(* Map a page table slot *)
+definition map_page_table_slot ::
+  "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
+   \<Rightarrow> cdl_object_id \<Rightarrow> word32 \<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
+  where
+  "map_page_table_slot spec orig_caps pd_id pt_id pt_vaddr free_cptr pt_slot  \<equiv> do
     frame_cap  \<leftarrow> assert_opt $ opt_cap (pt_id, pt_slot) spec;
     page       \<leftarrow> return $ cap_object frame_cap;
 
@@ -326,43 +303,94 @@ where
        Each page stores 12 bits of memory. *)
     page_vaddr   \<leftarrow> return $ pt_vaddr + (of_nat pt_slot << small_frame_size);
     page_rights  \<leftarrow> return (cap_rights frame_cap);
-    when (frame_cap \<noteq> NullCap)
-      (map_page spec orig_caps page pd_id page_rights page_vaddr)
+    if frame_cap \<noteq> NullCap then
+      do cptr  \<leftarrow> return $ free_cptr (pt_id, pt_slot);
+         map_page spec orig_caps page pd_id page_rights page_vaddr cptr
+      od
+    else
+      return ()
   od"
 
-(* Maps a page table's slots. *)
-definition map_page_table_slots :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
-                                                                  \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
-where
-  "map_page_table_slots spec orig_caps pd_id pd_slot \<equiv> do
+(* Map a page directory slot (and all its contents if it points to a page table) *)
+definition map_page_directory_slot ::
+  "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
+   \<Rightarrow> cdl_object_id \<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_cnode_index \<Rightarrow> unit u_monad"
+  where
+  "map_page_directory_slot spec orig_caps pd_id free_cptrs pd_slot \<equiv> do
     page_cap    \<leftarrow> assert_opt $ opt_cap (pd_id, pd_slot) spec;
-    page        \<leftarrow> return $ cap_object page_cap;
-    page_slots  \<leftarrow> return $ slots_of_list spec page;
+    page_id     \<leftarrow> return $ cap_object page_cap;
 
-    (* The page's virtual address is given by the number of slots and how much memory each maps.
+    (* The page table's virtual address is given by the number of slots and how much memory each maps.
        Each page directory slot maps 10+12 bits of memory (by the page table and page respectively). *)
     page_vaddr  \<leftarrow> return $ of_nat pd_slot << (pt_size + small_frame_size);
+    page_rights \<leftarrow> return (cap_rights page_cap);
 
-    when (fake_pt_cap_at (pd_id, pd_slot) spec)
-      (mapM_x (map_page_table_slot spec orig_caps pd_id page page_vaddr) page_slots)
+    if pt_at page_id spec then
+      do
+        map_page_table spec orig_caps page_id pd_id page_rights page_vaddr;
+        page_slots \<leftarrow> return $ slots_of_list spec page_id;
+        mapM_x (map_page_table_slot spec orig_caps pd_id page_id page_vaddr free_cptrs)
+               [slot <- page_slots. cap_at ((\<noteq>) NullCap) (page_id, slot) spec]
+      od
+    else if frame_at page_id spec then
+      do
+        cptr \<leftarrow> return $ free_cptrs (pd_id, pd_slot);
+        map_page spec orig_caps page_id pd_id page_rights page_vaddr cptr
+      od
+    else
+      return ()
   od"
 
-(* Maps a page directory and all its contents. *)
-definition map_page_directory_page_tables :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id
-                                                                                               \<Rightarrow> unit u_monad"
-where
-  "map_page_directory_page_tables spec orig_caps pd_id \<equiv> do
+(* Map a page directory and all its contents *)
+definition map_page_directory ::
+  "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option)
+   \<Rightarrow> (cdl_cap_ref \<Rightarrow> cdl_cptr) \<Rightarrow> cdl_object_id \<Rightarrow> unit u_monad"
+  where
+  "map_page_directory spec orig_caps free_cptrs pd_id \<equiv> do
     pd_slots \<leftarrow> return $ slots_of_list spec pd_id;
-    mapM_x (map_page_table_slots spec orig_caps pd_id) pd_slots
+    mapM_x (map_page_directory_slot spec orig_caps pd_id free_cptrs)
+           [pd_slot <- pd_slots. cap_at (\<lambda>cap. cap \<noteq> NullCap
+                                 \<and> frame_at (cap_object cap) spec) (pd_id, pd_slot) spec];
+    mapM_x (map_page_directory_slot spec orig_caps pd_id free_cptrs)
+           [pd_slot <- pd_slots. cap_at (\<lambda>cap. cap \<noteq> NullCap
+                                 \<and> pt_at (cap_object cap) spec) (pd_id, pd_slot) spec]
   od"
 
+(* Get a list of all the (object_id, slot) pairs contained within a page directory
+   and its child page tables which contain frame caps *)
+definition get_frame_caps :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> (cdl_object_id \<times> nat) list" where
+ "get_frame_caps spec pd_id \<equiv> do {
+    pd_slot <- slots_of_list spec pd_id;
+    obj_cap <- case_option [] (\<lambda>x. [x]) $ opt_cap (pd_id, pd_slot) spec;
+    let obj_id = cap_object obj_cap;
+    if frame_at obj_id spec then
+      [(pd_id, pd_slot)]
+    else
+      \<comment> \<open>If the slot contains a page table cap, collect all its slots that contain frames\<close>
+      map (Pair obj_id) o filter (\<lambda>slot. cap_at ((\<noteq>) NullCap) (obj_id, slot) spec) $
+        slots_of_list spec obj_id
+  }"
+
+(* Construct a function to assign each frame cap a free cptr, mapping all other slots to 0 *)
+definition make_frame_cap_map ::
+  "cdl_object_id list \<Rightarrow> word32 list \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id \<times> nat \<Rightarrow> word32"
+  where
+  "make_frame_cap_map obj_ids free_cptrs spec ref \<equiv>
+     case_option 0 id
+       (map_of (zip ([obj_id \<leftarrow> obj_ids. pd_at obj_id spec] \<bind> get_frame_caps spec) free_cptrs) ref)"
+
 (* Maps page directories and all their contents. *)
-definition init_vspace :: "cdl_state \<Rightarrow> (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow> cdl_object_id list \<Rightarrow> unit u_monad"
+definition init_vspace ::
+  "cdl_state \<Rightarrow>
+  (cdl_object_id \<Rightarrow> cdl_cptr option) \<Rightarrow>
+  cdl_object_id list \<Rightarrow>
+  cdl_cptr list \<Rightarrow>
+  unit u_monad"
 where
-  "init_vspace spec orig_caps obj_ids \<equiv> do
+  "init_vspace spec orig_caps obj_ids free_cptrs \<equiv> do
     pd_ids \<leftarrow> return [obj_id \<leftarrow> obj_ids. pd_at obj_id spec];
-    mapM_x (map_page_directory spec orig_caps) pd_ids;
-    mapM_x (map_page_directory_page_tables spec orig_caps) pd_ids
+    cptr_map \<leftarrow> return $ make_frame_cap_map obj_ids free_cptrs spec;
+    mapM_x (map_page_directory spec orig_caps cptr_map) pd_ids
   od"
 
 (**************************
@@ -480,7 +508,7 @@ where
 
     init_irqs     spec orig_caps irq_caps;
     init_pd_asids spec orig_caps obj_ids;
-    init_vspace   spec orig_caps obj_ids;
+    init_vspace   spec orig_caps obj_ids free_cptrs;
     init_tcbs     spec orig_caps obj_ids;
     init_cspace   spec orig_caps dup_caps irq_caps obj_ids;
     start_threads spec dup_caps obj_ids
diff --git a/sys-init/WellFormed_SI.thy b/sys-init/WellFormed_SI.thy
index 4d620b6fc..32aa65209 100644
--- a/sys-init/WellFormed_SI.thy
+++ b/sys-init/WellFormed_SI.thy
@@ -24,6 +24,7 @@ imports
   "DSpecProofs.Kernel_DP"
   "SepDSpec.Separation_SD"
   "Lib.SimpStrategy"
+  "AInvs.Rights_AI"
 begin
 
 context begin interpretation Arch . (*FIXME: arch_split*)
@@ -136,24 +137,6 @@ where
          | PageDirectoryCap _ _ ad \<Rightarrow> ad \<noteq> None
          | _                       \<Rightarrow> False)"
 
-definition is_real_vm_cap :: "cdl_cap \<Rightarrow> bool"
-where
-  "is_real_vm_cap cap \<equiv>
-       (case cap of
-           FrameCap _ _ _ _ Real _     \<Rightarrow> True
-         | PageTableCap _ Real _     \<Rightarrow> True
-         | PageDirectoryCap _ Real _ \<Rightarrow> True
-         | _                         \<Rightarrow> False)"
-
-definition is_fake_vm_cap :: "cdl_cap \<Rightarrow> bool"
-where
-  "is_fake_vm_cap cap \<equiv>
-       (case cap of
-           FrameCap _ _ _ _ Fake _     \<Rightarrow> True
-         | PageTableCap _ Fake _     \<Rightarrow> True
-         | PageDirectoryCap _ Fake _ \<Rightarrow> True
-         | _                         \<Rightarrow> False)"
-
 (* Original caps must have default rights,
  * and original endpoint + notification caps must not be badged.
  *)
@@ -385,7 +368,7 @@ lemma well_formed_cap_cap_has_object_eq:
 
 lemma well_formed_cap_update_cap_objects [simp]:
   "is_untyped_cap cap
-  \<Longrightarrow> well_formed_cap (update_cap_objects x cap) = well_formed_cap cap"
+   \<Longrightarrow> well_formed_cap (update_cap_objects x cap) = well_formed_cap cap"
   apply (clarsimp simp: update_cap_object_def
                         update_cap_objects_def well_formed_cap_def)
   apply (cases cap, simp_all)
@@ -399,8 +382,7 @@ lemma well_formed_cap_update_cap_object [simp]:
 
 lemma cap_rights_inter_default_cap_rights:
   "\<lbrakk>well_formed_cap cap; cap_type cap = Some type\<rbrakk>
-  \<Longrightarrow> cap_rights (default_cap type ids sz dev) \<inter> cap_rights cap
-    = cap_rights cap"
+   \<Longrightarrow> cap_rights (default_cap type ids sz dev) \<inter> cap_rights cap = cap_rights cap"
   by (fastforce simp: well_formed_cap_def default_cap_def cap_type_def cap_rights_def
                       validate_vm_rights_def vm_read_write_def
                       vm_kernel_only_def vm_read_only_def
@@ -444,7 +426,7 @@ lemma well_formed_distinct_slots_of_list [elim!]:
 
 lemma well_formed_object_size_bits:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> object_size_bits (object_default_state obj) = object_size_bits obj"
+   \<Longrightarrow> object_size_bits (object_default_state obj) = object_size_bits obj"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp)
@@ -452,13 +434,13 @@ lemma well_formed_object_size_bits:
 
 lemma well_formed_well_formed_caps:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> well_formed_caps spec obj_id obj"
+   \<Longrightarrow> well_formed_caps spec obj_id obj"
   by (clarsimp simp: well_formed_def split: option.splits)
 
 lemma well_formed_well_formed_cap:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
     object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> well_formed_cap cap"
+   \<Longrightarrow> well_formed_cap cap"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp simp: well_formed_caps_def)
@@ -475,13 +457,13 @@ lemma well_formed_well_formed_cap':
 
 lemma well_formed_well_formed_cap_to_object:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> well_formed_cap_to_object spec obj_id obj"
+   \<Longrightarrow> well_formed_cap_to_object spec obj_id obj"
   by (clarsimp simp: well_formed_def split: option.splits)
 
 lemma well_formed_well_formed_cap_to_real_object:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
     object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> well_formed_cap_to_real_object spec cap"
+   \<Longrightarrow> well_formed_cap_to_real_object spec cap"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp simp: well_formed_caps_def)
@@ -499,7 +481,7 @@ lemma well_formed_well_formed_cap_to_real_object':
 lemma well_formed_well_formed_cap_types_match:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
     object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> well_formed_cap_types_match spec cap"
+   \<Longrightarrow> well_formed_cap_types_match spec cap"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp simp: well_formed_caps_def)
@@ -516,7 +498,7 @@ lemma well_formed_well_formed_cap_types_match':
 
 lemma well_formed_cap_object_is_real:
   "\<lbrakk>well_formed spec; opt_cap slot spec = Some cap; cap_has_object cap\<rbrakk>
-  \<Longrightarrow> real_object_at (cap_object cap) spec"
+   \<Longrightarrow> real_object_at (cap_object cap) spec"
   apply (drule (1) well_formed_well_formed_cap_to_real_object', simp)
   apply (clarsimp simp: well_formed_cap_to_real_object_def)
   done
@@ -524,7 +506,7 @@ lemma well_formed_cap_object_is_real:
 lemma well_formed_types_match:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
     cdl_objects spec (cap_object cap) = Some cap_obj; cap_has_object cap\<rbrakk>
-  \<Longrightarrow> Some (object_type cap_obj) = cap_type cap"
+   \<Longrightarrow> Some (object_type cap_obj) = cap_type cap"
   apply (frule cap_has_object_not_NullCap)
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
@@ -538,7 +520,7 @@ lemma well_formed_types_match:
 
 lemma well_formed_object_slots:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> dom (object_slots obj) = dom (object_slots (object_default_state obj))"
+   \<Longrightarrow> dom (object_slots obj) = dom (object_slots (object_default_state obj))"
   apply (clarsimp simp: well_formed_def)
   apply (erule allE [where x=obj_id])
   apply simp
@@ -547,8 +529,7 @@ lemma well_formed_object_slots:
 lemma well_formed_slot_object_size_bits:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
     cdl_objects spec obj_id = Some obj; cnode_at obj_id spec\<rbrakk>
-  \<Longrightarrow> slot < 2 ^ object_size_bits obj"
-  apply (frule opt_cap_cdl_objects)
+   \<Longrightarrow> slot < 2 ^ object_size_bits obj"
   apply (clarsimp simp: well_formed_def object_at_def is_cnode_def)
   apply (erule_tac x=obj_id in allE)
   apply clarsimp
@@ -564,9 +545,26 @@ lemma well_formed_slot_object_size_bits:
   apply (clarsimp simp: object_slots_slots_of)
   done
 
+lemma well_formed_slot_object_size_bits_pt:
+  "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
+    pt_at obj_id spec; cdl_objects spec obj_id = Some obj\<rbrakk>
+   \<Longrightarrow> slot < 2 ^ object_size_bits obj"
+  apply (clarsimp simp: well_formed_def object_at_def is_pt_def)
+  apply (erule_tac x=obj_id in allE)
+  apply clarsimp
+  apply (subgoal_tac "slot \<in> dom (object_slots (object_default_state obj))")
+   apply (thin_tac "dom P = dom Q" for P Q)
+   apply (clarsimp simp: well_formed_caps_def)
+   apply (erule_tac x=slot in allE)
+   apply (clarsimp simp: object_default_state_def2 object_type_def has_slots_def
+                         default_tcb_def object_size_bits_def object_slots_def
+                         empty_cnode_def empty_cap_map_def pt_size_def pd_size_def
+                   split: cdl_object.splits if_split_asm)
+  by (fastforce intro: object_slots_opt_capI)
+
 lemma well_formed_cnode_object_size_bits:
   "\<lbrakk>well_formed spec; cnode_at obj_id spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> 0 < object_size_bits obj"
+   \<Longrightarrow> 0 < object_size_bits obj"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp simp: is_cnode_def object_at_def)
@@ -575,7 +573,7 @@ lemma well_formed_cnode_object_size_bits:
 lemma well_formed_cnode_object_size_bits_eq:
   "\<lbrakk>well_formed spec; opt_cap slot spec = Some cap;
     cdl_objects spec (cap_object cap) = Some obj; is_cnode_cap cap\<rbrakk>
-  \<Longrightarrow> object_size_bits obj = cnode_cap_size cap"
+   \<Longrightarrow> object_size_bits obj = cnode_cap_size cap"
   apply (frule (1) well_formed_cap_object_is_real)
    apply (clarsimp simp: cap_has_object_def cap_type_def split: cdl_cap.splits)
   apply (clarsimp simp: well_formed_def split_def split:option.splits)
@@ -603,7 +601,7 @@ lemma slots_of_set [simp]:
 
 lemma well_formed_well_formed_tcb:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> well_formed_tcb spec obj_id obj"
+   \<Longrightarrow> well_formed_tcb spec obj_id obj"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply clarsimp
@@ -611,7 +609,7 @@ lemma well_formed_well_formed_tcb:
 
 lemma well_formed_well_formed_vspace:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> well_formed_vspace spec obj_id obj"
+   \<Longrightarrow> well_formed_vspace spec obj_id obj"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply clarsimp
@@ -619,7 +617,7 @@ lemma well_formed_well_formed_vspace:
 
 lemma well_formed_well_formed_irq_node:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> well_formed_irq_node spec obj_id obj"
+   \<Longrightarrow> well_formed_irq_node spec obj_id obj"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply clarsimp
@@ -640,7 +638,7 @@ lemma well_formed_inj_cdl_irq_node:
 lemma well_formed_vm_cap_has_asid:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj;
     object_slots obj slot = Some cap\<rbrakk>
-  \<Longrightarrow> \<not>vm_cap_has_asid cap"
+   \<Longrightarrow> \<not>vm_cap_has_asid cap"
   apply (case_tac "cap = NullCap")
    apply (clarsimp simp: vm_cap_has_asid_def)
   apply (drule (3) well_formed_well_formed_cap)
@@ -655,27 +653,14 @@ lemma is_fake_vm_cap_cap_type:
   by (clarsimp simp: is_fake_vm_cap_def cap_type_def
               split: cdl_cap.splits)
 
-lemma well_formed_irq_node_in_irq_nodes:
-  "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj\<rbrakk>
-  \<Longrightarrow> obj_id \<in> irq_nodes spec"
-  oops
-
-term real_object_at
-lemma well_formed_irq_node_cap_is_ntfn_cap:
-  "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj;
-    object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> is_ntfn_cap cap"
-  apply (frule (3) well_formed_well_formed_cap_types_match)
-
-  apply (clarsimp simp: well_formed_cap_types_match_def)
-
-
-  oops
+lemma is_fake_vm_cap_cap_has_object[simp]:
+  "is_fake_vm_cap cap \<Longrightarrow> cap_has_object cap"
+  by (clarsimp simp: cap_has_object_def is_fake_vm_cap_def split: cdl_cap.splits)
 
 lemma well_formed_is_fake_vm_cap:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_cnode obj \<or> is_tcb obj \<or> is_irq_node obj;
     object_slots obj slot = Some cap\<rbrakk>
-  \<Longrightarrow> \<not>is_fake_vm_cap cap"
+   \<Longrightarrow> \<not>is_fake_vm_cap cap"
   apply (case_tac "is_irq_node obj")
    apply (frule (1) well_formed_well_formed_irq_node)
    apply (clarsimp simp: well_formed_irq_node_def object_at_def irq_nodes_def)
@@ -696,7 +681,7 @@ lemma vm_cap_has_asid_update_cap_object [simp]:
 
 lemma well_formed_object_size_bits_word_bits [simp]:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some spec_obj\<rbrakk>
-  \<Longrightarrow> object_size_bits spec_obj < word_bits"
+   \<Longrightarrow> object_size_bits spec_obj < word_bits"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply clarsimp
@@ -705,7 +690,7 @@ lemma well_formed_object_size_bits_word_bits [simp]:
 lemma well_formed_is_untyped_cap:
   "\<lbrakk>well_formed spec; cnode_at obj_id spec;
     opt_cap (obj_id, slot) spec = Some cap\<rbrakk>
-  \<Longrightarrow> \<not> is_untyped_cap cap"
+   \<Longrightarrow> \<not> is_untyped_cap cap"
   apply (frule opt_cap_cdl_objects)
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
@@ -719,7 +704,7 @@ lemma well_formed_is_untyped_cap:
 lemma well_formed_cap_has_object:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
    spec_cap \<noteq> NullCap; \<not> is_untyped_cap spec_cap; \<not> is_irqhandler_cap spec_cap\<rbrakk>
-  \<Longrightarrow> cap_has_object spec_cap"
+   \<Longrightarrow> cap_has_object spec_cap"
   apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def)
   apply (clarsimp simp: well_formed_def)
   apply (clarsimp split: option.splits)
@@ -736,7 +721,7 @@ lemma well_formed_cap_has_object:
 lemma well_formed_cap_object:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
     cap_has_object spec_cap\<rbrakk>
-  \<Longrightarrow> \<exists>obj. cdl_objects spec (cap_object spec_cap) = Some obj"
+   \<Longrightarrow> \<exists>obj. cdl_objects spec (cap_object spec_cap) = Some obj"
   apply (frule (1) well_formed_well_formed_cap', clarsimp)
   apply (frule (1) well_formed_cap_has_object)
     apply clarsimp
@@ -753,19 +738,19 @@ lemma well_formed_cap_object:
 lemma well_formed_cap_object_in_dom:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap;
     cap_has_object spec_cap\<rbrakk>
-  \<Longrightarrow> cap_object spec_cap \<in> dom (cdl_objects spec)"
+   \<Longrightarrow> cap_object spec_cap \<in> dom (cdl_objects spec)"
   by (drule (2) well_formed_cap_object, clarsimp)
 
 lemma well_formed_all_caps_cap_object:
   "\<lbrakk>well_formed spec; cap \<in> all_caps spec; cap_has_object cap\<rbrakk>
-  \<Longrightarrow>\<exists>obj. cdl_objects spec (cap_object cap) = Some obj"
+   \<Longrightarrow>\<exists>obj. cdl_objects spec (cap_object cap) = Some obj"
   apply (clarsimp simp: all_caps_def)
   apply (erule (2) well_formed_cap_object)
   done
 
 lemma well_formed_all_caps_cap_irq:
   "\<lbrakk>well_formed spec; cap \<in> all_caps spec; is_irqhandler_cap cap\<rbrakk>
-  \<Longrightarrow>\<exists>obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some obj"
+   \<Longrightarrow>\<exists>obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some obj"
   apply (clarsimp simp: all_caps_def)
   apply (frule (1) well_formed_well_formed_cap_types_match', simp)
   apply (clarsimp simp: well_formed_cap_types_match_def)
@@ -773,7 +758,7 @@ lemma well_formed_all_caps_cap_irq:
 
 lemma well_formed_update_cap_rights_idem:
   "\<lbrakk>well_formed_cap cap; rights = cap_rights cap\<rbrakk>
-  \<Longrightarrow> update_cap_rights rights cap = cap"
+   \<Longrightarrow> update_cap_rights rights cap = cap"
   by (auto simp: update_cap_rights_def cap_rights_def well_formed_cap_def
                validate_vm_rights_def vm_kernel_only_def vm_read_write_def
                vm_read_only_def split: cdl_cap.splits)
@@ -789,7 +774,7 @@ lemma default_ntfn_cap[simp]:
 
 lemma default_cap_well_formed_cap:
   "\<lbrakk>well_formed_cap cap; cap_type cap = Some type; cnode_cap_size cap = sz\<rbrakk>
-  \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev)"
+   \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev)"
   by (auto simp: well_formed_cap_def default_cap_def cap_type_def
                  word_gt_a_gt_0 vm_read_write_def cnode_cap_size_def
           split: cdl_cap.splits)
@@ -797,7 +782,7 @@ lemma default_cap_well_formed_cap:
 lemma default_cap_well_formed_cap2:
   "\<lbrakk>is_default_cap cap; cap_type cap = Some type; sz \<le> 32;
     \<not> is_untyped_cap cap; \<not> is_asidpool_cap cap\<rbrakk>
-  \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev )"
+   \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev )"
   apply (clarsimp simp: is_default_cap_def)
   apply (clarsimp simp: default_cap_def well_formed_cap_def
                         word_gt_a_gt_0 badge_bits_def guard_bits_def
@@ -809,7 +794,7 @@ lemma well_formed_well_formed_orig_cap:
   "\<lbrakk>well_formed spec;
     opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap;
     original_cap_at (obj_id, slot) spec\<rbrakk>
-  \<Longrightarrow> well_formed_orig_cap cap"
+   \<Longrightarrow> well_formed_orig_cap cap"
   apply (frule opt_cap_dom_cdl_objects)
   apply (clarsimp simp: dom_def, rename_tac obj)
   apply (frule (1) object_slots_opt_cap, simp)
@@ -828,7 +813,7 @@ lemma well_formed_orig_ep_cap_is_default:
   "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
     opt_cap (obj_id, slot) spec = Some cap;
     ep_related_cap cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> is_default_cap cap"
+   \<Longrightarrow> is_default_cap cap"
   apply (case_tac "\<exists>obj_id R. cap = ReplyCap obj_id R")
    apply (frule (1) well_formed_well_formed_cap', simp)
    apply (clarsimp simp: well_formed_cap_def)
@@ -847,7 +832,7 @@ lemma cap_rights_default_cap_eq:
 lemma well_formed_orig_caps:
   "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec;
     slots_of obj_id spec slot = Some cap; cap \<noteq> NullCap; cap_type cap = Some type\<rbrakk>
-  \<Longrightarrow> cap_rights (default_cap type obj_ids sz dev) = cap_rights cap"
+   \<Longrightarrow> cap_rights (default_cap type obj_ids sz dev) = cap_rights cap"
   apply (frule well_formed_well_formed_orig_cap, simp add: opt_cap_def, assumption+)
   apply (clarsimp simp: well_formed_orig_cap_def)
   apply (subst (asm) cap_rights_default_cap_eq, fast)
@@ -872,7 +857,7 @@ lemma well_formed_cdt:
 
 lemma well_formed_cap_to_real_object:
   "\<lbrakk>well_formed spec; real_object_at obj_id spec\<rbrakk>
-  \<Longrightarrow> \<exists>cnode_id slot cap.
+   \<Longrightarrow> \<exists>cnode_id slot cap.
        opt_cap (cnode_id, slot) spec = Some cap \<and>
        original_cap_at (cnode_id, slot) spec \<and>
        cnode_at cnode_id spec \<and>
@@ -885,7 +870,7 @@ lemma well_formed_cap_to_real_object:
 
 lemma well_formed_cap_to_irq_object:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; obj_id \<in> irq_nodes spec\<rbrakk>
-  \<Longrightarrow> \<exists>cnode_id slot cap.
+   \<Longrightarrow> \<exists>cnode_id slot cap.
        opt_cap (cnode_id, slot) spec = Some cap \<and>
        original_cap_at (cnode_id, slot) spec \<and>
        cnode_at cnode_id spec \<and>
@@ -898,7 +883,7 @@ lemma well_formed_cap_to_irq_object:
 lemma well_formed_cap_to_non_empty_pt:
   "\<lbrakk>well_formed spec; pt_at obj_id spec;
     object_at (\<lambda>obj. object_default_state obj \<noteq> obj) obj_id spec\<rbrakk>
-  \<Longrightarrow> \<exists>pd_id slot cap.
+   \<Longrightarrow> \<exists>pd_id slot cap.
        opt_cap (pd_id, slot) spec = Some cap \<and>
        pd_at pd_id spec \<and>
        cap_object cap = obj_id \<and>
@@ -915,21 +900,21 @@ lemma dom_object_slots_default_tcb:
 
 lemma well_formed_tcb_has_fault:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk>
-  \<Longrightarrow> \<not> cdl_tcb_has_fault tcb"
+   \<Longrightarrow> \<not> cdl_tcb_has_fault tcb"
   apply (drule (1) well_formed_well_formed_tcb)
   apply (clarsimp simp: well_formed_tcb_def tcb_has_fault_def)
   done
 
 lemma well_formed_tcb_domain:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk>
-  \<Longrightarrow> cdl_tcb_domain tcb = minBound"
+   \<Longrightarrow> cdl_tcb_domain tcb = minBound"
   apply (drule (1) well_formed_well_formed_tcb)
   apply (clarsimp simp: well_formed_tcb_def tcb_domain_def)
   done
 
 lemma well_formed_object_domain:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk>
-  \<Longrightarrow> object_domain obj = minBound"
+   \<Longrightarrow> object_domain obj = minBound"
   apply (case_tac "\<exists>tcb. obj = Tcb tcb")
    apply clarsimp
    apply (drule (1) well_formed_tcb_domain)
@@ -940,7 +925,7 @@ lemma well_formed_object_domain:
 
 lemma well_formed_tcb_object_slots:
   "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some tcb; is_tcb tcb\<rbrakk>
-  \<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}"
+   \<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}"
   apply (frule (1) well_formed_object_slots)
   apply (clarsimp simp: object_default_state_def2 is_tcb_def split: cdl_object.splits)
   apply (rule dom_object_slots_default_tcb)
@@ -949,7 +934,7 @@ lemma well_formed_tcb_object_slots:
 lemma well_formed_tcb_cspace_cap:
   "\<lbrakk>well_formed spec;
     tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> \<exists>cspace_cap. opt_cap (obj_id, tcb_cspace_slot) spec = Some cspace_cap \<and>
+   \<Longrightarrow> \<exists>cspace_cap. opt_cap (obj_id, tcb_cspace_slot) spec = Some cspace_cap \<and>
                    is_cnode_cap cspace_cap \<and> cap_guard_size cspace_cap \<noteq> 0 \<and>
                    real_object_at (cap_object cspace_cap) spec"
   apply (clarsimp simp: object_at_def)
@@ -973,7 +958,7 @@ lemma well_formed_tcb_cspace_cap:
 
 lemma cap_data_cap_guard_size_0:
   "\<lbrakk>well_formed_cap cap; is_cnode_cap cap; cap_data cap = 0\<rbrakk>
-  \<Longrightarrow> cap_guard_size cap = 0"
+   \<Longrightarrow> cap_guard_size cap = 0"
   apply (clarsimp simp: cap_type_def cap_data_def guard_as_rawdata_def
                         well_formed_cap_def
                  split: cdl_cap.splits)
@@ -993,7 +978,7 @@ lemma well_formed_tcb_cspace_cap_cap_data:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec;
     cdl_objects spec obj_id = Some (Tcb tcb);
     opt_cap (obj_id, tcb_cspace_slot) spec = Some spec_cspace_cap\<rbrakk>
-  \<Longrightarrow> cap_data spec_cspace_cap \<noteq> 0"
+   \<Longrightarrow> cap_data spec_cspace_cap \<noteq> 0"
   apply (frule (1) well_formed_tcb_cspace_cap, clarsimp)
   apply (frule (1) well_formed_well_formed_cap', clarsimp)
   apply (drule (2) cap_data_cap_guard_size_0, simp)
@@ -1001,7 +986,7 @@ lemma well_formed_tcb_cspace_cap_cap_data:
 
 lemma well_formed_tcb_opt_cap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec; slot \<in> {0..tcb_boundntfn_slot}\<rbrakk>
-  \<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap"
+   \<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap"
   apply (clarsimp simp: object_at_def)
   apply (drule (1) well_formed_object_slots)
   apply (fastforce simp: object_default_state_def2 is_tcb_def
@@ -1014,7 +999,7 @@ lemma well_formed_tcb_opt_cap:
 lemma well_formed_tcb_vspace_cap:
   "\<lbrakk>well_formed spec;
     tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> \<exists>vspace_cap.
+   \<Longrightarrow> \<exists>vspace_cap.
     opt_cap (obj_id, tcb_vspace_slot) spec = Some vspace_cap \<and> is_pd_cap vspace_cap"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_vspace_slot], simp add: tcb_slot_defs)
   apply (clarsimp simp: object_at_def)
@@ -1025,7 +1010,7 @@ lemma well_formed_tcb_vspace_cap:
 lemma well_formed_tcb_ipcbuffer_cap:
   "\<lbrakk>well_formed spec;
     tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> \<exists>tcb_ipcbuffer_cap.
+   \<Longrightarrow> \<exists>tcb_ipcbuffer_cap.
     opt_cap (obj_id, tcb_ipcbuffer_slot) spec = Some tcb_ipcbuffer_cap \<and>
     is_default_cap tcb_ipcbuffer_cap \<and> is_frame_cap tcb_ipcbuffer_cap"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_ipcbuffer_slot], simp add: tcb_slot_defs)
@@ -1036,7 +1021,7 @@ lemma well_formed_tcb_ipcbuffer_cap:
 
 lemma well_formed_tcb_caller_cap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> opt_cap (obj_id, tcb_caller_slot) spec = Some NullCap"
+   \<Longrightarrow> opt_cap (obj_id, tcb_caller_slot) spec = Some NullCap"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_caller_slot], simp add: tcb_slot_defs)
   apply (clarsimp simp: object_at_def)
   apply (frule (1) well_formed_well_formed_tcb)
@@ -1045,7 +1030,7 @@ lemma well_formed_tcb_caller_cap:
 
 lemma well_formed_tcb_replycap_cap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some NullCap \<or>
+   \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some NullCap \<or>
       opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_replycap_slot], simp add: tcb_slot_defs)
   apply (clarsimp simp: object_at_def)
@@ -1056,7 +1041,7 @@ lemma well_formed_tcb_replycap_cap:
 
 lemma well_formed_tcb_pending_op_cap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some NullCap \<or>
+   \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some NullCap \<or>
       opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_pending_op_slot], simp add: tcb_slot_defs)
   apply (clarsimp simp: object_at_def)
@@ -1066,7 +1051,7 @@ lemma well_formed_tcb_pending_op_cap:
 
 lemma well_formed_tcb_pending_op_replycap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> (opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id))
+   \<Longrightarrow> (opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id))
     = (opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap)"
   apply (clarsimp simp: object_at_def)
   apply (drule (1) well_formed_well_formed_tcb)
@@ -1075,7 +1060,7 @@ lemma well_formed_tcb_pending_op_replycap:
 
 lemma well_formed_tcb_boundntfn_cap:
   "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk>
-  \<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap"
+   \<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap"
   apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_boundntfn_slot], simp add: tcb_slot_defs)
   apply (elim exE)
   apply (clarsimp simp: object_at_def)
@@ -1087,7 +1072,7 @@ lemma well_formed_orig_caps_unique:
     cnode_at obj_id spec; cnode_at obj_id' spec; cap_has_object cap; cap_has_object cap';
     opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
     cap_object cap = cap_object cap'\<rbrakk>
-  \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
+   \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
   by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def)
 
 lemma well_formed_orig_caps_unique':
@@ -1096,19 +1081,19 @@ lemma well_formed_orig_caps_unique':
     opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
     cap_has_object cap; cap_has_object cap';
     cap_object cap = cap_object cap'\<rbrakk>
-  \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
+   \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
   by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def real_cap_ref_def)
 
 lemma well_formed_irqhandler_caps_unique:
   "\<lbrakk>well_formed s; is_irqhandler_cap cap; is_irqhandler_cap cap';
     opt_cap (obj_id, slot) s = Some cap; opt_cap (obj_id', slot') s = Some cap';
     cap_irq cap = cap_irq cap'\<rbrakk>
-  \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
+   \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
   by (clarsimp simp: well_formed_def well_formed_irqhandler_caps_unique_def)
 
 lemma object_cap_ref_cap_irq:
   "\<lbrakk>object_cap_ref (obj_id, slot) spec; opt_cap (obj_id, slot) spec = Some cap\<rbrakk>
-  \<Longrightarrow> cap_irq cap = undefined"
+   \<Longrightarrow> cap_irq cap = undefined"
   by (auto simp: object_cap_ref_def cap_has_object_def cap_irq_def
           split: cdl_cap.splits)
 
@@ -1122,7 +1107,7 @@ lemma well_formed_orig_caps_unique_object_cap:
     opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap';
     cap_has_object cap; cap_has_object cap';
     cap_object cap = cap_object cap'\<rbrakk>
-  \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
+   \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'"
   apply (frule object_cap_ref_real_cap_ref, drule (1) object_cap_ref_cap_irq)+
   apply (erule (8) well_formed_orig_caps_unique', simp)
   done
@@ -1130,7 +1115,7 @@ lemma well_formed_orig_caps_unique_object_cap:
 lemma well_formed_child_cap_not_copyable:
   "\<lbrakk>well_formed spec; \<not> original_cap_at (obj_id, slot) spec;
     opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> is_copyable_cap cap"
+   \<Longrightarrow> is_copyable_cap cap"
   apply (clarsimp simp: well_formed_def)
   apply (erule_tac x=obj_id in allE)
   apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def)
@@ -1142,13 +1127,13 @@ lemma well_formed_child_cap_not_copyable:
 lemma well_formed_child_cap_not_copyable':
   "\<lbrakk>well_formed spec;
     opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> \<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap"
+   \<Longrightarrow> \<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap"
   by (rule impI, erule (3) well_formed_child_cap_not_copyable)
 
 lemma well_formed_pd:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
     pd_at obj_id spec; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> is_frame_cap cap \<or> is_fake_pt_cap cap"
+   \<Longrightarrow> is_frame_cap cap \<or> is_fake_pt_cap cap"
   apply (clarsimp simp: object_at_def)
   apply (frule (1) well_formed_well_formed_vspace)
   apply (clarsimp simp: well_formed_vspace_def)
@@ -1160,7 +1145,7 @@ lemma well_formed_pd:
 lemma well_formed_pt:
   "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap;
     pt_at obj_id spec; cap \<noteq> NullCap\<rbrakk>
-  \<Longrightarrow> is_frame_cap cap"
+   \<Longrightarrow> is_frame_cap cap"
   apply (clarsimp simp: object_at_def)
   apply (frule (1) well_formed_well_formed_vspace)
   apply (clarsimp simp: well_formed_vspace_def)
@@ -1175,6 +1160,26 @@ lemma well_formed_pt_cap_is_fake_pt_cap:
    \<Longrightarrow> is_fake_pt_cap cap"
   by (frule (2) well_formed_pd, clarsimp+)
 
+lemma wf_cap_pt_cap[simp]: "well_formed_cap (PageTableCap pt_id ty addr) \<longleftrightarrow> addr = None"
+  by (clarsimp simp: well_formed_cap_def)
+
+lemma wf_frame_cap_frame_size_bits:
+  "\<lbrakk>well_formed spec;
+    opt_cap (pt_ptr, slot) spec = Some (FrameCap dev frame_ptr rights n Fake None);
+    cdl_objects spec frame_ptr = Some (Frame frame)\<rbrakk>
+   \<Longrightarrow> cdl_frame_size_bits frame = n"
+  apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits)
+  apply (frule (2) well_formed_well_formed_cap_types_match, fastforce)
+  apply (fastforce simp: well_formed_cap_types_match_def cap_object_def object_type_def)
+  done
+
+lemma wf_pd_cap_has_object:
+  "\<lbrakk>well_formed spec;
+    pd_at spec_pd_ptr spec;
+    opt_cap (spec_pd_ptr, slot) spec = Some cap;
+    cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap_has_object cap"
+  by (fastforce simp: cap_has_object_def cap_type_def is_fake_pt_cap_def
+                dest: well_formed_pd split: cdl_cap.splits)
 
 
 (****************************************
@@ -1237,7 +1242,7 @@ lemma well_formed_irq_nodes_cdl_irq_node:
 
 lemma well_formed_cdl_irq_node_irq_nodes:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
-  \<Longrightarrow> cdl_irq_node spec irq \<in> irq_nodes spec"
+   \<Longrightarrow> cdl_irq_node spec irq \<in> irq_nodes spec"
   apply (drule well_formed_well_formed_irq_table)
   apply (clarsimp simp: well_formed_irq_table_def)
   apply (fastforce simp: object_at_def)
@@ -1245,14 +1250,14 @@ lemma well_formed_cdl_irq_node_irq_nodes:
 
 lemma well_formed_irq_is_irq_node:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
-  \<Longrightarrow> is_irq_node irq_node"
+   \<Longrightarrow> is_irq_node irq_node"
   apply (frule (1) well_formed_cdl_irq_node_irq_nodes)
   apply (clarsimp simp: irq_nodes_def object_at_def)
   done
 
 lemma well_formed_object_slots_irq_node:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
-  \<Longrightarrow> dom (object_slots irq_node) = {0}"
+   \<Longrightarrow> dom (object_slots irq_node) = {0}"
   apply (frule (1) well_formed_cdl_irq_node_irq_nodes)
   apply (frule (1) well_formed_well_formed_irq_node)
   apply (clarsimp simp: well_formed_irq_node_def)
@@ -1262,7 +1267,7 @@ lemma well_formed_irq_ntfn_cap:
   "\<lbrakk>well_formed spec;
     irq \<in> bound_irqs spec;
     opt_cap (cdl_irq_node spec irq, 0) spec = Some ntfn_cap\<rbrakk>
-  \<Longrightarrow> ntfn_cap = NotificationCap (cap_object ntfn_cap) 0 {AllowRead, AllowWrite}"
+   \<Longrightarrow> ntfn_cap = NotificationCap (cap_object ntfn_cap) 0 {AllowRead, AllowWrite}"
   apply (frule opt_cap_cdl_objects, clarsimp)
   apply (frule (1) well_formed_object_slots_irq_node [where irq=irq])
   apply (frule (1) well_formed_well_formed_irq_node)
@@ -1284,7 +1289,7 @@ lemma well_formed_bound_irqs_are_used_irqs:
 
 lemma well_formed_slots_of_used_irq_node:
   "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
-  \<Longrightarrow> dom (slots_of (cdl_irq_node spec irq) spec) = {0}"
+   \<Longrightarrow> dom (slots_of (cdl_irq_node spec irq) spec) = {0}"
   apply (clarsimp simp: used_irqs_def slots_of_def opt_object_def split: option.splits)
   apply (frule (2) well_formed_all_caps_cap_irq, clarsimp)
   apply (erule (1) well_formed_object_slots_irq_node)
@@ -1292,14 +1297,14 @@ lemma well_formed_slots_of_used_irq_node:
 
 lemma well_formed_slot_0_of_used_irq_node:
   "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
-  \<Longrightarrow> \<exists>ntfn_cap. slots_of (cdl_irq_node spec irq) spec 0 = Some ntfn_cap"
+   \<Longrightarrow> \<exists>ntfn_cap. slots_of (cdl_irq_node spec irq) spec 0 = Some ntfn_cap"
   apply (frule (1) well_formed_slots_of_used_irq_node)
   apply (clarsimp simp: dom_eq_singleton_conv)
   done
 
 lemma well_formed_object_slots_default_irq_node:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
-  \<Longrightarrow> dom (object_slots (object_default_state irq_node)) = {0}"
+   \<Longrightarrow> dom (object_slots (object_default_state irq_node)) = {0}"
   by (metis well_formed_object_slots well_formed_object_slots_irq_node)
 
 lemma object_slots_empty_cnode:
@@ -1315,7 +1320,7 @@ lemma dom_empty_cap_map_singleton:
 
 lemma well_formed_size_irq_node:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk>
-  \<Longrightarrow> object_size_bits irq_node = 0"
+   \<Longrightarrow> object_size_bits irq_node = 0"
   apply (frule (1) well_formed_irq_is_irq_node)
   apply (frule (1) well_formed_object_slots)
   apply (drule (1) well_formed_object_slots_default_irq_node)
@@ -1326,14 +1331,14 @@ lemma well_formed_size_irq_node:
 
 lemma well_formed_used_irqs_have_irq_node:
   "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk>
-  \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
+   \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
   apply (clarsimp simp: used_irqs_def)
   apply (erule (2) well_formed_all_caps_cap_irq)
   done
 
 lemma well_formed_bound_irqs_have_irq_node:
   "\<lbrakk>well_formed spec; irq \<in> bound_irqs spec\<rbrakk>
-  \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
+   \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node"
   apply (frule well_formed_well_formed_irqhandler_caps)
   apply (clarsimp simp: well_formed_irqhandler_caps_def used_irqs_def bound_irqs_def all_caps_def)
   done
@@ -1341,7 +1346,7 @@ lemma well_formed_bound_irqs_have_irq_node:
 lemma well_formed_irq_node_is_bound:
   "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node;
     object_slots irq_node 0 \<noteq> Some NullCap\<rbrakk>
-  \<Longrightarrow> irq \<in> bound_irqs spec"
+   \<Longrightarrow> irq \<in> bound_irqs spec"
   apply (frule well_formed_well_formed_irqhandler_caps)
   apply (frule (1) well_formed_object_slots_default_irq_node)
   apply (frule (1) well_formed_object_slots)
@@ -1376,7 +1381,7 @@ lemma well_formed_cap_object_cdl_irq_node:
 (* There are no untyped objects (as there are no untyped caps). *)
 lemma well_formed_object_untyped:
  "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some object\<rbrakk>
-  \<Longrightarrow> object_type object \<noteq> UntypedType"
+   \<Longrightarrow> object_type object \<noteq> UntypedType"
   apply (case_tac "real_object_at obj_id spec")
    apply (frule (1) well_formed_cap_to_real_object)
    apply clarsimp
@@ -1411,7 +1416,7 @@ lemma well_formed_no_asidpools:
 
 lemma well_formed_fake_pt_cap_in_pd:
   "\<lbrakk>well_formed spec; slots_of obj_id spec slot = Some cap; is_fake_pt_cap cap\<rbrakk>
-  \<Longrightarrow> pd_at obj_id spec"
+   \<Longrightarrow> pd_at obj_id spec"
   apply (clarsimp simp: slots_of_def opt_object_def split: option.splits)
   apply (rename_tac obj)
   apply (frule well_formed_asidpool_at [where obj_id=obj_id])
@@ -1428,6 +1433,18 @@ lemma well_formed_fake_pt_cap_in_pd:
   apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_slots_def)
   done
 
+lemma well_formed_pt_cap_pt_at:
+  "\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some cap; is_fake_pt_cap cap\<rbrakk>
+   \<Longrightarrow> pt_at (cap_object cap) spec"
+  apply (case_tac cap_ref, clarsimp)
+  apply (frule (1) well_formed_cap_object)
+   apply (fastforce intro: is_fake_pt_cap_cap_has_object)
+  apply clarsimp
+  apply (frule (2) well_formed_types_match)
+   apply (fastforce intro: is_fake_pt_cap_cap_has_object)
+  apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_at_def object_type_is_object)
+  done
+
 lemma cap_has_object_cap_irq [simp]:
   "cap_has_object cap \<Longrightarrow> cap_irq cap = undefined"
   by (auto simp: cap_has_object_def cap_irq_def split: cdl_cap.splits)
@@ -1573,7 +1590,7 @@ lemma well_formed_objects_only_real_or_irq:
 
 lemma well_formed_objects_card:
   "\<lbrakk>well_formed spec \<rbrakk>
-  \<Longrightarrow> card (used_irqs spec) + card {x. real_object_at x spec} = card (dom (cdl_objects spec))"
+   \<Longrightarrow> card (used_irqs spec) + card {x. real_object_at x spec} = card (dom (cdl_objects spec))"
   apply (frule well_formed_inj_cdl_irq_node)
   apply (frule well_formed_objects_real_or_irq)
   apply (frule well_formed_objects_only_real_or_irq)
@@ -1673,6 +1690,153 @@ lemma update_cap_data:
   apply simp
   done
 
+lemma well_formed_frame_in_pt:
+  "\<lbrakk>well_formed spec;
+    opt_cap (pt, pt_slot) spec = Some frame_cap;
+    frame_cap \<noteq> NullCap;
+    pt_at pt spec\<rbrakk>
+   \<Longrightarrow> \<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and>
+           (sz = 12 \<or> sz = 16) \<and>
+           is_fake_vm_cap frame_cap"
+  apply (clarsimp simp: well_formed_def object_at_def)
+  apply (drule_tac x = pt in spec)
+  apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
+                 split: option.split_asm)
+  done
+
+lemma well_formed_frame_in_pd:
+  "\<lbrakk>well_formed spec;
+    opt_cap (pd, pt_slot) spec = Some frame_cap;
+    pd_at pd spec;
+    is_frame_cap frame_cap\<rbrakk>
+   \<Longrightarrow> (\<exists>sz. cap_type frame_cap = Some (FrameType sz) \<and> (sz = 20 \<or> sz = 24)) \<and>
+      is_fake_vm_cap frame_cap \<and>
+      \<not> is_device_cap frame_cap"
+  apply (clarsimp simp: well_formed_def object_at_def)
+  apply (drule_tac x = pd in spec)
+  apply (clarsimp simp: well_formed_vspace_def opt_cap_def slots_of_def opt_object_def
+                 split: option.split_asm)
+  apply (drule_tac x = pt_slot in spec)
+  apply (drule_tac x = frame_cap in spec)
+  apply (clarsimp simp: is_fake_pt_cap_def cap_type_def
+                 split: cdl_cap.splits)
+  apply (clarsimp simp: cap_at_def opt_cap_def slots_of_def opt_object_def
+              simp del: split_paired_All)
+  apply (drule_tac x = pd in spec)
+  apply (drule_tac x = pt_slot in spec)
+  apply fastforce
+  done
+
+lemma well_formed_no_dev: "well_formed spec \<Longrightarrow> \<forall>slot. \<not> cap_at is_device_cap slot spec"
+  by (clarsimp simp: well_formed_def)
+
+lemma well_formed_frame_cap[simp]:
+  "well_formed_cap (FrameCap x y rights a b R) \<longleftrightarrow>
+     R = None \<and> (rights = vm_read_write \<or> rights = vm_read_only)"
+  apply (clarsimp simp: well_formed_cap_def split: cdl_frame_cap_type.splits)
+  apply (rule iffI; clarsimp?)
+  done
+
+lemma wf_cap_in_pt_is_frame:
+  "well_formed spec \<Longrightarrow>
+   page_cap \<noteq> NullCap \<Longrightarrow>
+   pt_at pt_id spec \<Longrightarrow>
+   opt_cap (pt_id, slot) spec = Some page_cap \<Longrightarrow>
+   page_cap = fake_frame_cap False (cap_object page_cap)
+                                   (validate_vm_rights (cap_rights page_cap))
+                                   (cap_size_bits page_cap) \<and>
+  (cap_size_bits page_cap = 12 \<or> cap_size_bits page_cap = 16)"
+  apply (frule well_formed_frame_in_pt, fastforce+)
+  apply (clarsimp simp: cap_type_def cap_rights_def cap_size_bits_def split: cdl_cap.splits)
+  apply (frule well_formed_well_formed_cap[where obj_id=pt_id])
+     apply (fastforce intro: object_slots_opt_capI)+
+  apply clarsimp
+  apply (drule well_formed_no_dev, clarsimp simp: cap_at_def)
+  apply (fastforce simp: fake_vm_cap_simp)
+  done
+
+lemma wf_frame_cap_in_pd:
+  "well_formed spec \<Longrightarrow>
+   page_cap \<noteq> NullCap \<Longrightarrow>
+   pd_at pd_id spec \<Longrightarrow>
+   opt_cap (pd_id, slot) spec = Some page_cap \<Longrightarrow>
+   frame_at (cap_object page_cap) spec \<Longrightarrow>
+   page_cap = fake_frame_cap False (cap_object page_cap)
+                                   (validate_vm_rights (cap_rights page_cap))
+                                   (cap_size_bits page_cap) \<and>
+   (cap_size_bits page_cap = 20 \<or> cap_size_bits page_cap = 24)"
+  apply (frule well_formed_frame_in_pd, fastforce+)
+   apply (frule well_formed_types_match, fastforce+)
+    using object_type_is_object(9) object_type_object_at(9) wf_pd_cap_has_object apply blast
+   apply (frule object_at_object_type(10)[rotated], rule classical, fastforce)
+   apply (fastforce simp: cap_type_def split: cdl_cap.splits)
+  apply (clarsimp simp: cap_type_def cap_rights_def cap_size_bits_def split: cdl_cap.splits)
+  apply (frule well_formed_well_formed_cap[where obj_id=pd_id])
+     apply fastforce
+    apply (fastforce intro: object_slots_opt_capI)
+   apply (fastforce simp: fake_vm_cap_simp)+
+  done
+
+lemma wf_pt_in_pd_fake_and_none:
+  "well_formed spec \<Longrightarrow>
+   page_cap \<noteq> NullCap \<Longrightarrow>
+   pd_at pd_id spec \<Longrightarrow>
+   opt_cap (pd_id, slot) spec = Some page_cap \<Longrightarrow>
+   pt_at (cap_object page_cap) spec \<Longrightarrow>
+   page_cap = PageTableCap (cap_object page_cap) Fake None"
+  apply (clarsimp simp: object_at_def)
+  apply (frule well_formed_types_match[where obj_id=pd_id and slot=slot])
+     apply fastforce+
+     using object_at_def wf_pd_cap_has_object
+   apply blast
+  apply (clarsimp simp: object_type_is_object)
+  apply (frule well_formed_pt_cap_is_fake_pt_cap[where obj_id=pd_id and slot=slot])
+     apply fastforce
+    apply (clarsimp simp: object_at_def)
+    apply (clarsimp simp: object_type_is_object)
+   apply (frule (1) well_formed_well_formed_cap[where obj_id=pd_id and slot=slot])
+     apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits)
+     apply fastforce+
+  apply (clarsimp simp: cap_type_def is_fake_pt_cap_pt_cap split: cdl_cap.splits)
+  using well_formed_well_formed_cap' wf_cap_pt_cap by blast
+
+lemma well_formed_pd_slots_have_objects:
+  "\<lbrakk>well_formed spec; pd_at pd_id spec; slot \<in> dom (slots_of pd_id spec);
+    slots_of pd_id spec slot = Some cap; cap \<noteq> NullCap\<rbrakk>
+   \<Longrightarrow> cap_has_object cap"
+  apply (drule (1) wf_pd_cap_has_object[where cap=cap and slot=slot])
+    apply (clarsimp simp: opt_cap_def)+
+  done
+
+lemma well_formed_pd_slot_limited:
+  "\<lbrakk>well_formed spec; pd_at obj_id spec; slots_of obj_id spec slot = Some cap\<rbrakk>
+   \<Longrightarrow> slot < 4096"
+  apply (clarsimp simp:well_formed_def object_at_def)
+  apply (drule_tac x = obj_id in spec)
+  apply (clarsimp simp: is_pd_def object_type_simps object_default_state_def slots_of_def,
+              simp add: default_object_def object_type_simps opt_object_def object_slots_def empty_cap_map_def
+                 split: cdl_object.split_asm option.split_asm)
+  apply fastforce
+  done
+
+lemma well_formed_pd_frame_or_pt:
+  "well_formed spec \<Longrightarrow>
+   pd_at pd_ptr spec \<Longrightarrow>
+   opt_cap (pd_ptr,slot) spec = Some slot_cap \<Longrightarrow>
+   cap_object slot_cap = ptr \<Longrightarrow>
+   slot_cap \<noteq> NullCap \<Longrightarrow>
+   frame_at ptr spec \<noteq> pt_at ptr spec"
+  apply (frule (3) well_formed_pd[where obj_id=pd_ptr and slot=slot])
+  apply clarsimp
+  apply (frule (3) wf_pd_cap_has_object)
+  apply (frule (2) well_formed_cap_object)
+  apply clarsimp
+  apply (safe; (fastforce simp: object_at_def dest: not_frame_and_pt)?)
+   apply (frule well_formed_types_match[where obj_id=pd_ptr and slot=slot], fastforce+)
+   apply (fastforce simp: object_type_is_object(10) intro: object_at_cdl_objects)
+  apply (frule well_formed_types_match[where obj_id=pd_ptr and slot=slot], fastforce+)
+  using is_fake_pt_cap_is_pt_cap object_type_is_object(8) by (fastforce intro: object_at_cdl_objects)
+
 end
 
 end