diff --git a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
index b200db1d9..9eaf27251 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
@@ -367,7 +367,7 @@ lemma vspace_objs':
   "valid_vspace_objs s \<Longrightarrow> valid_vspace_objs s'"
   using ko
   apply (clarsimp simp: valid_vspace_objs_def vs_lookup')
-(*  apply (fastforce simp: obj_at_def)*)
+(*  apply (fastforce simp: obj_at_def split: arch_kernel_obj.splits) *)
   sorry
 
 lemma caps_of_state_s':
@@ -646,7 +646,7 @@ lemma cap_insert_ap_invs:
   apply (auto simp: obj_at_def is_tcb_def is_cap_table_def a_type_def
                     valid_cap_def [where c="cap.Zombie a b x" for a b x]
               dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits)
-(*  apply (clarsimp simp: obj_at_def a_type_def)*)
+(*  apply (fastforce simp: obj_at_def a_type_def)*)
   sorry
 
 
@@ -1035,7 +1035,6 @@ lemma shiftr_irrelevant:
   apply simp
   done
 
-
 lemma create_mapping_entries_parent_for_refs:
   "\<lbrace>invs and \<exists>\<rhd> pd and page_directory_at pd
            and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz)
@@ -1044,7 +1043,7 @@ lemma create_mapping_entries_parent_for_refs:
                  rights attribs pd
    \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -"
   apply (rule hoare_gen_asmE)+
-  apply (cases pgsz, simp_all add: vmsz_aligned_def)
+  apply (cases pgsz, simp_all add: vmsz_aligned_def largePagePTE_offsets_def superSectionPDE_offsets_def)
      apply (rule hoare_pre)
       apply wp
       apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to)
@@ -1055,22 +1054,28 @@ lemma create_mapping_entries_parent_for_refs:
      apply wp
      apply (rule hoare_post_imp_R)
       apply (rule lookup_pt_slot_cap_to_multiple1)
+     apply (simp only: add.commute)
      apply (elim conjE exEI cte_wp_at_weakenE)
-     apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
-                           subset_iff p_0x3C_shift vspace_bits_defs largePagePTE_offsets_def
-                     split: ARM_A.arch_cap.splits)
-(*   apply (rule hoare_pre, wp)
+     apply_trace (simp add: pte_bits_def del: set_map cap_asid_simps not_None_eq)
+     apply_trace (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
+                           subset_iff p_0x3C_shift
+                     simp del: cap_asid_simps set_map del: imageE)
+     apply (erule_tac x=t in allE)
+     apply (subgoal_tac "map (op + r) [0 , 8 .e. 0x78] = [r , r + 8 .e. r + 0x78]", simp)
+defer
+   apply simp
+   apply (rule hoare_pre, wp)
    apply (clarsimp dest!:vs_lookup_pages_vs_lookupI)
    apply (drule valid_vs_lookupD, clarsimp)
    apply (simp, elim exEI)
    apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
                          lookup_pd_slot_def Let_def)
-   apply (subst pd_shifting, simp add: pd_bits_def pageBits_def)
-   apply (clarsimp simp: vs_cap_ref_def
+   apply (subst pd_shifting, simp add: vspace_bits_defs)
+   apply (clarsimp simp: vs_cap_ref_def simp del: cap_asid_simps
                   split: cap.split_asm arch_cap.split_asm option.split_asm)
      apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
                 dest!: caps_of_state_valid_cap)[3]
-     apply (frule(1) caps_of_state_valid)
+(*     apply (frule(1) caps_of_state_valid)
      apply (clarsimp simp:valid_cap_def obj_at_def)
    apply (simp add:is_cap_simps)
   apply (rule hoare_pre, wp)
diff --git a/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
index 3c968212b..88bc45a26 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
@@ -280,8 +280,8 @@ lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]:
       valid_asid_map_def
       pspace_in_kernel_window_def cap_refs_in_kernel_window_def
       cur_tcb_def sym_refs_def state_refs_of_def state_hyp_refs_of_def vspace_at_asid_def
-      swp_def valid_irq_states_def)
-  sorry
+      swp_def valid_irq_states_def split: option.splits)
+  done
 
 
 lemma cte_at_nat_to_cref_zbits [CNodeInv_AI_assms]:
@@ -523,9 +523,10 @@ lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
   apply (rename_tac arch_cap)
   apply (case_tac arch_cap, simp_all add: arch_finalise_cap_def)
       apply (wp
-           | clarsimp simp: valid_cap_def split: option.split bool.split
+           | clarsimp simp: valid_cap_def obj_at_def is_tcb_def is_cap_table_def
+                      split: option.splits bool.split
            | intro impI conjI)+
-  sorry (* add vcpu case *)
+  done
 
 
 crunch emptyable[wp, CNodeInv_AI_assms]: finalise_cap "emptyable sl"
@@ -689,7 +690,7 @@ next
     apply (clarsimp simp add: invs_def valid_state_def
       invs_valid_objs invs_psp_aligned)
     apply (drule(1) if_unsafe_then_capD, clarsimp+)
-    sorry
+    done
 next
   have replicate_helper:
     "\<And>x n. True \<in> set x \<Longrightarrow> replicate n False \<noteq> x"
@@ -1010,7 +1011,7 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
             | simp del: split_paired_Ex split_paired_All
             | simp add: valid_irq_node_def valid_machine_state_def
                    del: split_paired_All split_paired_Ex)+
-(*   apply (clarsimp simp: tcb_cap_valid_def cte_wp_at_caps_of_state)
+   apply (clarsimp simp: tcb_cap_valid_def cte_wp_at_caps_of_state)
    apply (frule(1) valid_global_refsD2[where ptr=ptr])
    apply (frule(1) cap_refs_in_kernel_windowD[where ptr=ptr])
    apply (frule weak_derived_cap_range)
@@ -1019,11 +1020,12 @@ lemma cap_move_invs[wp, CNodeInv_AI_assms]:
    apply (simp add: is_cap_simps)
    apply (subgoal_tac "tcb_cap_valid cap.NullCap ptr s")
     apply (simp add: tcb_cap_valid_def)
+    defer
    apply (rule tcb_cap_valid_NullCapD)
     apply (erule(1) tcb_cap_valid_caps_of_stateD)
    apply (simp add: is_cap_simps)
   apply (clarsimp simp: cte_wp_at_caps_of_state)
-  done *)sorry (* hyp_ref *)
+  sorry
 
 end
 
diff --git a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
index bd9258870..7e6d90385 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
@@ -48,14 +48,14 @@ lemma vs_lookup_pages_eq:
   "\<lbrakk>valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s;
     valid_cap cap s; table_cap_ref cap = Some vref; oref \<in> obj_refs cap\<rbrakk>
    \<Longrightarrow> (vref \<unrhd> oref) s = (vref \<rhd> oref) s"
-  apply (clarsimp simp: table_cap_ref_def
+  apply (clarsimp simp: table_cap_ref_def arch_cap_fun_lift_def
                         vs_lookup_pages_eq_at[symmetric, THEN fun_cong]
                         vs_lookup_pages_eq_ap[symmetric, THEN fun_cong]
                  split: cap.splits arch_cap.splits option.splits)
   apply (rule iffI[rotated, OF vs_lookup_pages_vs_lookupI], assumption)
   apply (simp add: valid_cap_def)
   apply (erule vs_lookup_vs_lookup_pagesI', clarsimp+)
-  sorry
+  done
 
 lemma nat_to_cref_unat_of_bl':
   "\<lbrakk> length xs < 32; n = length xs \<rbrakk> \<Longrightarrow>
@@ -269,7 +269,72 @@ lemma (* empty_slot_invs *) [Finalise_AI_asms]:
   apply (simp add: empty_slot_def set_cdt_def bind_assoc cong: if_cong)
   apply (wp opt_deleted_irq_handler_invs)
         apply (simp add: invs_def valid_state_def valid_mdb_def2)
-  sorry
+        apply (wp replace_cap_valid_pspace set_cap_caps_of_state2
+                  replace_cap_ifunsafe get_cap_wp
+                  set_cap_idle valid_irq_node_typ set_cap_typ_at
+                  set_cap_irq_handlers set_cap_valid_arch_caps
+                  set_cap_cap_refs_respects_device_region_NullCap
+                  | simp add: trans_state_update[symmetric] del: trans_state_update fun_upd_apply split del: split_if )+
+  apply (clarsimp simp: is_final_cap'_def2 simp del: fun_upd_apply)
+  apply (clarsimp simp: conj_comms invs_def valid_state_def valid_mdb_def2)
+  apply (subgoal_tac "mdb_empty_abs s")
+   prefer 2
+   apply (rule mdb_empty_abs.intro)
+   apply (rule vmdb_abs.intro)
+   apply (simp add: valid_mdb_def swp_def cte_wp_at_caps_of_state conj_comms)
+  apply (clarsimp simp: untyped_mdb_def mdb_empty_abs.descendants mdb_empty_abs.no_mloop_n
+                        valid_pspace_def cap_range_def)
+  apply (clarsimp simp: untyped_inc_def mdb_empty_abs.descendants mdb_empty_abs.no_mloop_n)
+  apply (simp add: ut_revocable_def cur_tcb_def valid_irq_node_def
+                   no_cap_to_obj_with_diff_ref_Null)
+  apply (rule conjI)
+   apply (clarsimp simp: cte_wp_at_cte_at)
+  apply (rule conjI)
+   apply (clarsimp simp: irq_revocable_def)
+  apply (rule conjI)
+   apply (clarsimp simp: reply_master_revocable_def)
+  apply (thin_tac "\<forall>irq. irqopt = Some irq \<longrightarrow> P irq" for P)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_machine_state_def)
+  apply (rule conjI)
+   apply (clarsimp simp:descendants_inc_def mdb_empty_abs.descendants)
+  apply (rule conjI)
+   apply (clarsimp simp: reply_mdb_def)
+   apply (rule conjI)
+    apply (unfold reply_caps_mdb_def)[1]
+    apply (rule allEI, assumption)
+    apply (fold reply_caps_mdb_def)[1]
+    apply (case_tac "sl = ptr", simp)
+    apply (simp add: fun_upd_def split del: split_if del: split_paired_Ex)
+    apply (erule allEI, rule impI, erule(1) impE)
+    apply (erule exEI)
+    apply (simp, rule ccontr)
+    apply (erule(5) emptyable_no_reply_cap)
+    apply simp
+   apply (unfold reply_masters_mdb_def)[1]
+   apply (elim allEI)
+   apply (clarsimp simp: mdb_empty_abs.descendants)
+  apply (rule conjI)
+   apply (simp add: valid_ioc_def)
+  apply (rule conjI)
+   apply (clarsimp simp: tcb_cap_valid_def
+                  dest!: emptyable_valid_NullCapD)
+  apply (rule conjI)
+   apply (clarsimp simp: mdb_cte_at_def cte_wp_at_caps_of_state)
+   apply (cases sl)
+   apply (rule conjI, clarsimp)
+    apply (subgoal_tac "cdt s \<Turnstile> (ab,bb) \<rightarrow> (ab,bb)")
+     apply (simp add: no_mloop_def)
+    apply (rule r_into_trancl)
+    apply (simp add: cdt_parent_of_def)
+   apply fastforce
+  apply (clarsimp simp: cte_wp_at_caps_of_state replaceable_def
+                        vs_cap_ref_simps table_cap_ref_simps
+                   del: allI)
+  apply (case_tac "is_final_cap' cap s")
+   apply auto[1]
+  apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state)
+  done
 
 lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]:
   "dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs :: machine_word) < 5}"
@@ -299,6 +364,35 @@ lemma deleting_irq_handler_final [Finalise_AI_asms]:
   apply simp
   done
 
+lemma arch_thread_set_final_cap[wp]:
+  "\<lbrace>is_final_cap' cap\<rbrace> arch_thread_set v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
+  apply (simp add: arch_thread_set_def is_final_cap'_def2 cte_wp_at_caps_of_state)
+  apply wp
+  apply (simp add: set_object_def, wp)
+  apply (case_tac "get_tcb t s"; simp)
+  apply (clarsimp simp add:  split: option.splits)
+  sorry
+
+lemma arch_thread_get_final_cap[wp]:
+  "\<lbrace>is_final_cap' cap\<rbrace> arch_thread_get v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
+  apply (simp add: arch_thread_get_def is_final_cap'_def2 cte_wp_at_caps_of_state, wp)
+  apply auto
+  done
+
+lemma dissociate_vcpu_tcb_final_cap[wp]:
+  "\<lbrace>is_final_cap' cap\<rbrace> dissociate_vcpu_tcb v t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>"
+  apply (simp add: dissociate_vcpu_tcb_def)
+  apply wp
+  sorry
+
+
+lemma prepare_thread_delete_final[wp]:
+  "\<lbrace>is_final_cap' cap\<rbrace> prepare_thread_delete t \<lbrace> \<lambda>rv. is_final_cap' cap\<rbrace>"
+  unfolding prepare_thread_delete_def
+  apply (wp  hoare_drop_imps
+       | wpc | clarsimp simp add: tcb_cap_cases_def)+
+  done
+
 lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s
          \<and> cte_wp_at (op = cap) slot s\<rbrace>
@@ -325,10 +419,10 @@ lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]:
                                   appropriate_cte_cap_def
                                   vs_cap_ref_def
                       | intro impI TrueI ext conjI)+
-(*  apply (simp add: arch_finalise_cap_def)
+  apply (simp add: arch_finalise_cap_def)
   apply (rule hoare_pre)
-   apply (wp | wpc | simp only: simp_thms)+ *)
-  sorry
+   apply (wp | wpc | simp only: simp_thms)+
+  done
 
 crunch typ_at_arch [wp]: arch_thread_set "\<lambda>s. P (typ_at T p s)"
   (wp: crunch_wps set_object_typ_at)
@@ -482,12 +576,33 @@ lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]:
                  dest!: obj_ref_none_no_asid[rule_format])
   done
 
+lemma dissociate_vcpu_tcb_no_cap_to_obj_ref[wp]:
+  "\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
+     dissociate_vcpu_tcb v t
+   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
+  unfolding dissociate_vcpu_tcb_def
+  apply wp
+sorry
+
+lemma prepare_thread_delete_no_cap_to_obj_ref[wp]:
+  "\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
+     prepare_thread_delete t
+   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
+  unfolding prepare_thread_delete_def
+  apply (wp hoare_drop_imp hoare_vcg_all_lift | wpc)+
+  apply auto
+  sorry
+
+lemma prepare_thread_delete_unlive[wp]:
+  "\<lbrace>\<lambda>_. True\<rbrace> prepare_thread_delete ptr \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ptr\<rbrace>"
+  sorry
+
 lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
   "\<lbrace>\<lambda>s. s \<turnstile> cap \<and> x = is_final_cap' cap s \<and> valid_mdb s
         \<and> cte_wp_at (op = cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
         \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
         \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
-                               valid_arch_objs s \<and>
+                               valid_vspace_objs s \<and>
                                valid_arch_state s)\<rbrace>
      finalise_cap cap x
    \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
@@ -499,6 +614,7 @@ lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
             apply (rule hoare_pre)
             apply ((wp suspend_unlive[unfolded o_def]
                       suspend_final_cap[where sl=sl]
+                      prepare_thread_delete_unlive[unfolded o_def]
                       unbind_maybe_notification_not_bound
                       get_ntfn_ko
                       unbind_notification_valid_objs
@@ -526,13 +642,13 @@ lemma (* finalise_cap_replaceable *) [Finalise_AI_asms]:
                    | wpc
                    | simp add: valid_cap_simps is_nondevice_page_cap_simps)+)
   apply (rule hoare_chain)
-(*    apply (rule arch_finalise_cap_replaceable[where sl=sl])
+    apply (rule arch_finalise_cap_replaceable[where sl=sl])
    apply (clarsimp simp: replaceable_def reachable_pg_cap_def
                          o_def cap_range_def valid_arch_state_def
                          ran_tcb_cap_cases is_cap_simps
                          obj_irq_refs_subset vs_cap_ref_def)+
-  apply (fastforce split: option.splits vmpage_size.splits) *)
-  sorry
+  apply (fastforce split: option.splits vmpage_size.splits)
+  done
 
 lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]:
   assumes x: "\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap"
@@ -544,9 +660,11 @@ lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]:
 crunch cte_wp_at[wp,Finalise_AI_asms]: dissociate_vcpu_tcb "\<lambda>s. P (cte_wp_at P' p s)"
   (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
 
-crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
+crunch cte_wp_at[wp,Finalise_AI_asms]: prepare_thread_delete "\<lambda>s. P (cte_wp_at P' p s)"
   (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
 
+crunch cte_wp_at[wp,Finalise_AI_asms]: arch_finalise_cap "\<lambda>s. P (cte_wp_at P' p s)"
+  (simp: crunch_simps assertE_def wp: crunch_wps set_object_cte_at ignore: arch_thread_set)
 end
 
 interpretation Finalise_AI_1?: Finalise_AI_1
@@ -599,9 +717,12 @@ context Arch begin global_naming ARM
 crunch irq_node[wp]: vcpu_switch "\<lambda>s. P (interrupt_irq_node s)"
   (wp: crunch_wps select_wp simp: crunch_simps)
 
-crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
+crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\<lambda>s. P (interrupt_irq_node s)"
   (wp: crunch_wps select_wp simp: crunch_simps)
 
+crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
+  (simp: crunch_simps wp: crunch_wps)
+
 crunch pred_tcb_at[wp]: arch_finalise_cap "pred_tcb_at proj P t"
   (simp: crunch_simps wp: crunch_wps)
 
@@ -611,18 +732,18 @@ lemma tcb_cap_valid_pagetable:
     = tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot"
   apply (rule ext)
   apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_nondevice_page_cap_arch_def
-                   is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_arch_def
+                   is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
             split: Structures_A.thread_state.split)
-  sorry
+  done
 
 lemma tcb_cap_valid_pagedirectory:
   "tcb_cap_valid (ArchObjectCap (PageDirectoryCap word (Some v))) slot
     = tcb_cap_valid (ArchObjectCap (PageDirectoryCap word None)) slot"
   apply (rule ext)
   apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_nondevice_page_cap_arch_def
-                   is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_arch_def
+                   is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
             split: Structures_A.thread_state.split)
-  sorry
+  done
 
 lemma store_pde_unmap_empty:
   "\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
@@ -636,6 +757,9 @@ lemma store_pde_unmap_empty:
 crunch empty[wp]: find_free_hw_asid, store_hw_asid, load_hw_asid, set_vm_root_for_flush, page_table_mapped, invalidate_tlb_by_asid
   "\<lambda>s. obj_at (empty_table {}) word s"
 
+crunch empty[wp]: vcpu_switch
+  "\<lambda>s. obj_at (empty_table {}) word s"
+
 lemma store_pte_unmap_empty:
   "\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
     store_pte xa InvalidPTE
@@ -663,12 +787,12 @@ lemma flush_table_empty:
     flush_table ac aa b word
    \<lbrace>\<lambda>rv s. obj_at (empty_table {}) word s\<rbrace>"
   apply (clarsimp simp: flush_table_def set_vm_root_def)
-  apply (wp do_machine_op_obj_at arm_context_switch_empty hoare_whenE_wp
+  apply (wp do_machine_op_obj_at arm_context_switch_empty hoare_whenE_wp hoare_drop_imp
     | wpc
     | simp
     | wps)+
   apply (rename_tac pd x y)
-(*  apply (rule_tac Q="\<lambda>pd' s.
+  apply (rule_tac Q="\<lambda>pd' s.
               (if pd \<noteq> pd'
                then (\<lambda>s. obj_at
                          (empty_table {}) word
@@ -688,8 +812,8 @@ lemma flush_table_empty:
     | wpc
     | rule_tac
         Q="\<lambda>_ s. obj_at (empty_table {}) word s"
-        in hoare_strengthen_post)+ *)
-  sorry
+        in hoare_strengthen_post)+
+  done
 
 lemma unmap_page_table_empty:
   "\<lbrace>\<lambda>s. obj_at (empty_table {}) word s\<rbrace>
@@ -699,15 +823,15 @@ lemma unmap_page_table_empty:
   apply (wp store_pde_unmap_empty flush_table_empty page_table_mapped_empty | simp | wpc)+
   done
 
-lemma mapM_x_store_pte_valid_arch_objs:
+lemma mapM_x_store_pte_valid_vspace_objs:
   "\<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and>
     (\<forall>x \<in> set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap)) \<rbrace>
     mapM_x (\<lambda>p. store_pte p InvalidPTE) pteptrs
-   \<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
+   \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
   apply (rule hoare_strengthen_post)
    apply (wp  mapM_x_wp')
     apply (fastforce simp: is_pt_cap_def)+
-  sorry
+  done
 
 lemma mapM_x_swp_store_empty_table_set:
   "\<lbrace>page_table_at p
@@ -719,8 +843,9 @@ lemma mapM_x_swp_store_empty_table_set:
   apply (rule hoare_strengthen_post)
    apply (rule mapM_x_swp_store_empty_table)
   apply (clarsimp simp: obj_at_def empty_table_def)
-  apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits)
-  sorry
+  apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits option.splits)
+  apply (clarsimp simp add: valid_pde_mappings_def pde_ref_def)
+  done
 
 definition
   replaceable_or_arch_update
@@ -872,19 +997,13 @@ lemma delete_asid_empty_table_pd:
       \<and> obj_at (empty_table {}) word s\<rbrace>
     delete_asid a word
    \<lbrace>\<lambda>_ s. obj_at (empty_table {}) word s\<rbrace>"
-(*   apply (simp add: delete_asid_def)
+   apply (simp add: delete_asid_def)
    apply (wp | wpc)+
-         apply wps
-         apply wp
        apply (simp add: set_asid_pool_def)
        apply wp
-         apply (case_tac "x2 = word")
-          defer
-          apply wps
-          apply (rule set_object_at_obj)
          apply (wp get_object_ret | wps)+
-   apply (clarsimp simp: obj_at_def empty_table_def)+*)
-  sorry
+   apply (clarsimp simp: obj_at_def empty_table_def)+
+  done
 
 lemma page_directory_at_def2:
   "page_directory_at p s = (\<exists>pd. ko_at (ArchObj (PageDirectory pd)) p s)"
@@ -933,40 +1052,23 @@ lemma obj_at_empty_tableI:
   \<Longrightarrow> obj_at (empty_table {}) p s"
   apply safe
   apply (simp add: obj_at_def empty_table_def pde_wp_at_def)
-(*  (* Boring cases *)
+  (* Boring cases *)
   apply (case_tac "\<exists>ko. kheap s p = Some ko")
    apply (erule exE) apply (rule_tac x=ko in exI)
    apply (rule conjI)
     apply assumption
    apply (case_tac ko)
        apply ((erule_tac x="ucast (kernel_base >> 21) - 1" in allE,
-         simp add: kernel_base_def kernel_mapping_slots_def)+)[4]
+         simp add: kernel_base_def)+)[4]
    apply (rename_tac arch_kernel_obj)
    apply (case_tac arch_kernel_obj) defer 3
       apply ((erule_tac x="ucast (kernel_base >> 21) - 1" in allE,
-         simp add: kernel_base_def kernel_mapping_slots_def)+)[4]
+         simp add: kernel_base_def)+)[5]
    (* Interesting case *)
   apply (rename_tac "fun")
   apply clarsimp
-  apply (erule_tac x=x in allE)
-  apply (case_tac "x \<notin> kernel_mapping_slots")
-   apply (simp add:valid_pde_mappings_def pde_ref_def)
-  apply simp
-  apply (rule conjI)
-   apply (simp add: invs_def valid_state_def valid_kernel_mappings_def
-                    valid_kernel_mappings_if_pd_def)
-   apply (erule conjE)+
-   apply (erule_tac x="ArchObj (PageDirectory fun)" in ballE)
-    apply simp
-   apply (simp add: ran_def)
-  apply (clarsimp simp: invs_def valid_state_def valid_arch_state_def
-                        equal_kernel_mappings_def
-                        obj_at_def a_type_simps)
-   apply (erule_tac x=p in allE,
-          erule_tac x="arm_global_pd (arch_state s)" in allE)
-   apply (erule_tac x="fun" in allE, erule_tac x="pd" in allE)
-   apply (simp add: empty_table_def) *)
-  sorry
+  apply (clarsimp simp add: valid_pde_mappings_def pde_ref_def)
+  done
 
 lemma pd_shifting_again3:
   "is_aligned pd pd_bits \<Longrightarrow> ((ucast (ae :: 11 word) << 3) + (pd :: word32) && ~~ mask pd_bits) = pd"
@@ -1027,23 +1129,24 @@ lemma mapM_x_store_pde_InvalidPDE_empty:
     defer
     apply (rule allI)
     apply (erule_tac x="ucast x" in ballE)
-(*     apply (rule impI)
+(*     apply (rule impI)*)
      apply (frule_tac pd="word" and ae="x" in pd_shifting_again3)
      apply (frule_tac pd="word" and ae="x" in pd_shifting_again5)
-      apply ((simp add: kernel_mapping_slots_def kernel_base_def)+)[3]
-    apply (subst word_not_le)
+      apply ((simp add: kernel_base_def)+)[3]
+
+
+(*    apply (subst word_not_le) *)
     apply (subst (asm) word_not_le)
-    apply (cut_tac x="ucast x" and y="kernel_base >> 20" in le_m1_iff_lt)
-    apply clarsimp
+    apply (cut_tac x="ucast x" and y="kernel_base >> 21" in le_m1_iff_lt)
     apply (simp add: le_m1_iff_lt word_less_nat_alt unat_ucast)
-    apply (simp add: pde_ref_def)
-   apply (rule conjI, rule allI, rule impI)
+(*    apply (simp add: pde_ref_def) *)
+(*   apply (rule conjI, rule allI, rule impI)
     apply (rule pd_shifting_kernel_mapping_slots)
-     apply simp+
-   apply (rule allI, rule impI)
+     apply simp+*)
+(*   apply (rule allI, rule impI)
    apply (rule pd_shifting_global_refs)
      apply simp+
-  apply (wp store_pde_pde_wp_at2)*)
+  apply (wp store_pde_pde_wp_at2) *)
   sorry
 
 lemma word_aligned_pt_slots:
@@ -1188,11 +1291,11 @@ lemma replaceable_or_arch_update_pg:
   apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
   done
 
-lemma store_pde_arch_objs_invalid: (* ARMHYP do we need this? *)
+(*lemma store_pde_arch_objs_invalid: (* ARMHYP do we need this? *)
   "\<lbrace>valid_arch_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
-(*  apply (wp store_pde_arch_objs_unmap)
-  apply (simp add: pde_ref_def) *)
-  sorry
+  apply (wp store_pde_arch_objs_unmap)
+  apply (simp add: pde_ref_def)
+  done *)
 
 lemma store_pde_vspace_objs_invalid:
   "\<lbrace>valid_vspace_objs\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
diff --git a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
index a4a4d63a5..35434a18c 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
@@ -347,6 +347,13 @@ lemmas
   wellformed_arch_obj_simps[simp] =
   wellformed_arch_obj_def[split_simps arch_kernel_obj.split]
 
+lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>wellformed_arch_obj ao s; kheap s = kheap s'\<rbrakk>
+          \<Longrightarrow> wellformed_arch_obj ao s'"
+  apply (case_tac ao, simp_all)
+  apply (simp add: obj_at_def valid_vcpu_def split: option.splits)
+  done
+
+
 section "Virtual Memory"
 
 definition (* ARMHYP *)
@@ -1131,6 +1138,13 @@ by (rule kernel_object_exhaust[of ko]; clarsimp simp add: a_type_simps split: if
 lemmas aa_type_elims[elim!] =
    aa_type_AASIDPoolE aa_type_APageDirectoryE aa_type_APageTableE aa_type_ADeviceDataE aa_type_AUserDataE aa_type_AVCPUE
 
+lemma wellformed_arch_typ:
+   assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
+   shows   "\<lbrace>\<lambda>s. wellformed_arch_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. wellformed_arch_obj ao s\<rbrace>"
+  apply (cases ao; clarsimp simp: valid_vcpu_def split: option.splits; wp?)
+  apply (rule conjI; clarsimp; wp P)
+done
+
 lemma valid_arch_obj_pspaceI:
   "\<lbrakk> valid_arch_obj obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_obj obj s'"
   apply (cases obj, simp_all)
diff --git a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy
index d1966c8a4..3fe6890a7 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy
@@ -267,9 +267,9 @@ lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \
 
 lemma make_arch_fault_msg_invs[wp]: "\<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace>"
   apply (cases f)
-  apply simp
+  apply simp_all
   apply wp
-  sorry (* add ARMHYP specific cases *)
+  done
 
 lemma make_fault_message_inv[wp, Ipc_AI_assms]:
   "\<lbrace>P\<rbrace> make_fault_msg ft t \<lbrace>\<lambda>rv. P\<rbrace>"
@@ -436,6 +436,21 @@ lemma do_ipc_transfer_tcb_caps [Ipc_AI_assms]:
 
 crunch typ_at[Ipc_AI_assms]: handle_arch_fault_reply "P (typ_at T p s)"
 
+lemma transfer_caps_loop_valid_vspace_objs[wp, Ipc_AI_assms]:
+  "\<lbrace>valid_vspace_objs\<rbrace>
+      transfer_caps_loop ep buffer n caps slots mi
+    \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
+  apply (induct caps arbitrary: slots n mi, simp)
+  apply (clarsimp simp: Let_def split_def whenE_def
+                  cong: if_cong list.case_cong
+             split del: split_if)
+  apply (rule hoare_pre)
+   apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
+              derive_cap_is_derived_foo
+             hoare_drop_imps
+        | assumption | simp split del: split_if)+
+  done
+
 end
 
 interpretation Ipc_AI?: Ipc_AI
@@ -473,8 +488,11 @@ lemma do_ipc_transfer_respects_device_region[Ipc_AI_cont_assms]:
    apply auto
    done
 
+crunch state_hyp_refs_of[wp]: set_mrs "\<lambda> s. P (state_hyp_refs_of s)"
+  (wp: crunch_wps simp: zipWithM_x_mapM ignore: set_object transfer_caps_loop)
+
 crunch state_hyp_refs_of[wp, Ipc_AI_cont_assms]: do_ipc_transfer "\<lambda> s. P (state_hyp_refs_of s)"
-  (wp: crunch_wps simp: zipWithM_x_mapM ignore: transfer_caps_loop)
+  (wp: crunch_wps simp: zipWithM_x_mapM)
 
 
 end
diff --git a/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy
index b0b98ee41..a754f9129 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchKHeap_AI.thy
@@ -283,18 +283,6 @@ lemma vs_lookup_pages_vspace_obj_at_lift:
   by (auto simp: vs_refs_pages.vspace_only
            intro!: vspace_obj_pred_fI[where f=Ex])
 
-(* ARMHYP not needed?
-lemma valid_arch_objs_lift_weak:
-  assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow>
-                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
-  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
-  shows "\<lbrace>valid_arch_objs\<rbrace> f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>" (* ARMHYP *)
-  apply (rule valid_arch_objs_lift)
-   apply (rule valid_vspace_objs_lift)
-     apply (rule vs_lookup_arch_obj_at_lift)
-      apply (rule obj_at arch_state; simp)+
-  apply (simp add: obj_at_def)
- done *)
 
 lemma valid_vspace_objs_lift_weak:
   assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
@@ -581,34 +569,6 @@ lemma valid_machine_state_lift:
   apply simp
   done
 
-(*
-lemma bool_pred_exhaust:
-  "(P = (\<lambda>x. x)) \<or> (P = (\<lambda>x. \<not>x)) \<or> (P = (\<lambda>_. True)) \<or> (P = (\<lambda>_. False))"
-  apply (cases "P True"; cases "P False")
-  apply (rule disjI2, rule disjI2, rule disjI1, rule ext)
-  defer
-  apply (rule disjI1, rule ext)
-  defer
-  apply (rule disjI2, rule disjI1, rule ext)
-  defer
-  apply (rule disjI2, rule disjI2, rule disjI2, rule ext)
-  apply (match conclusion in "P x = _" for x \<Rightarrow> \<open>cases x; fastforce\<close>)+
-  done
-*)
-(*
-lemma valid_ao_at_lift:
-  assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
-      and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
-  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
-  unfolding valid_ao_at_def
-  by (wp hoare_vcg_ex_lift y valid_arch_obj_typ z)
-
-lemma valid_ao_at_lift_aobj_at:
-  assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
-  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
-  unfolding valid_ao_at_def
-  by (wp hoare_vcg_ex_lift valid_arch_obj_typ aobj_at | clarsimp)+
-*)
 lemma valid_vso_at_lift:
   assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
       and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
@@ -801,5 +761,81 @@ lemma cap_is_device_obj_is_device[simp]:
 
 crunch device_state_inv: storeWord "\<lambda>ms. P (device_state ms)"
 
+
+(* some hyp_ref invariants *)
+
+lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow>
+       state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s"
+  apply (rule all_ext)
+  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
+  done
+
+lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
+       state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
+  apply (rule all_ext)
+  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
+  done
+
+lemma state_hyp_refs_of_tcb_bound_ntfn_update:
+       "kheap s t = Some (TCB tcb) \<Longrightarrow>
+          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
+            = state_hyp_refs_of s"
+  apply (rule all_ext)
+  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
+  done
+
+lemma state_hyp_refs_of_tcb_state_update:
+       "kheap s t = Some (TCB tcb) \<Longrightarrow>
+          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
+            = state_hyp_refs_of s"
+  apply (rule all_ext)
+  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
+  done
+
+lemma valid_arch_obj_same_type:
+  "\<lbrakk>valid_arch_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
+  \<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
+  apply (induction ao rule: arch_kernel_obj.induct;
+         clarsimp simp: valid_arch_obj.simps typ_at_same_type)
+    apply (rule hoare_to_pure_kheap_upd; assumption?)
+      apply (rule valid_pte_lift, assumption)
+     apply blast
+    apply (simp add: obj_at_def)
+   apply (rule hoare_to_pure_kheap_upd; assumption?)
+     apply (rule valid_pde_lift, assumption)
+    apply blast
+   apply (simp add: obj_at_def)
+  apply (simp add: valid_vcpu_def split: option.splits)
+  apply (drule typ_at_same_type[rotated]; assumption)
+done
+
+lemma valid_vcpu_lift:
+  assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
+  assumes t: "\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>rv. typ_at ATCB p\<rbrace>"
+  shows "\<lbrace>\<lambda>s. valid_vcpu v s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vcpu v s\<rbrace>"
+  apply (cases v)
+  apply (simp add: valid_vcpu_def | wp x hoare_vcg_disj_lift)+
+  apply (case_tac vcpu_tcb; simp, wp t)
+  done
+
+
+lemma valid_vcpu_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
+       state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
+  apply (rule all_ext)
+  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
+  done
+
+lemma valid_vcpu_same_type:
+  "\<lbrakk> valid_vcpu v s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
+   \<Longrightarrow> valid_vcpu v (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
+  by (cases v; case_tac vcpu_tcb; clarsimp simp: valid_vcpu_def typ_at_same_type)
+
+lemma wellformed_arch_obj_same_type:
+  "\<lbrakk> wellformed_arch_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
+   \<Longrightarrow> wellformed_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
+  by (induction ao rule: arch_kernel_obj.induct;
+         clarsimp simp: valid_arch_obj.simps typ_at_same_type valid_vcpu_same_type)
+
+
 end
 end
diff --git a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy
index 079f06a05..11cd46ff1 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy
@@ -138,6 +138,8 @@ lemma checked_insert_tcb_invs[wp]: (* arch specific *)
   apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps)
   done
 
+crunch caps_of_state[wp]: prepare_thread_delete "\<lambda>s. P (caps_of_state s)"
+  (wp: mapM_x_wp' crunch_wps)
 
 lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
   assumes x: "P cap.NullCap"
@@ -145,15 +147,16 @@ lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
                 finalise_cap cap fin
               \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
   apply (cases cap, simp_all)
-       apply (wp suspend_caps_of_state hoare_vcg_all_lift
+       apply (wp prepare_thread_delete_caps_of_state hoare_vcg_all_lift
+                 suspend_caps_of_state
             | simp
             | rule impI
             | rule hoare_drop_imps)+
-     apply (clarsimp simp: ball_ran_eq x)
+(*     apply (clarsimp simp: ball_ran_eq x)
     apply (wp delete_one_caps_of_state
          | rule impI
          | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+
-    sorry (* prepare_thread_delete *)
+*)  sorry
 
 
 lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]:
@@ -181,6 +184,7 @@ lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
   apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
   done
 
+declare arch_cap_fun_lift_simps [simp del]
 lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
   "\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
      cap_delete slot
@@ -191,9 +195,14 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
   apply simp
   apply (rule use_spec)
   apply (rule rec_del_all_caps_in_range)
+       apply (simp add: atomize_imp)
      apply_trace (simp add: table_cap_ref_def[simplified, split_simps cap.split]
-                       del: arch_cap_fun_lift_simps
-              | rule obj_ref_none_no_asid)+
+                             vspace_bits_defs
+                       del: arch_cap_fun_lift_non_arch
+                       split del: arch_cap.split
+                       cong: cap.case_cong_weak)+
+(*     apply (rule_tac obj_ref_none_no_asid) *)
+
   sorry
 
 lemma as_user_valid_cap[wp]:
@@ -240,7 +249,7 @@ lemma tc_invs[Tcb_AI_asms]:
   apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
   apply (rule hoare_vcg_precond_imp)
    apply wp
-      apply ((simp only: simp_thms
+      apply_trace ((simp only: simp_thms
         | rule wp_split_const_if wp_split_const_if_R
                    hoare_vcg_all_lift_R
                    hoare_vcg_E_elim hoare_vcg_const_imp_lift_R
diff --git a/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy
index b11b2182e..c5ff17b48 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchUntyped_AI.thy
@@ -134,31 +134,26 @@ proof -
       apply (erule range_cover.sz)
      apply (simp add:range_cover_def)
     apply (clarsimp simp:get_free_ref_def is_aligned_neg_mask_eq empty_descendants_range_in)
+    apply (rule conjI[rotated], blast, clarsimp)
     apply (drule_tac x = "(obj_ref_of node_cap,nat_to_cref (bits_of node_cap) slota)" in bspec)
      apply (clarsimp simp:is_cap_simps nat_to_cref_def word_bits_def
        bits_of_def valid_cap_simps cap_aligned_def)+
-(*   apply (frule(1) range_cover_stuff[where sz = sz])
+   apply (simp add: free_index_of_def)
+   apply (frule(1) range_cover_stuff[where sz = sz])
      apply (clarsimp dest!:valid_cap_aligned simp:cap_aligned_def word_bits_def)+
     apply simp+
-   apply (clarsimp simp:get_free_ref_def) *)
-(*   apply (frule cte_wp_at_caps_descendants_range_inI
-     [where ptr = w and sz = sz and idx = 0 and cref = slot])
-       subgoal by (clarsimp simp:cte_wp_at_caps_of_state is_aligned_neg_mask_eq)
-      subgoal by simp
-     subgoal by (simp add:range_cover_def word_bits_def)
-    subgoal by (simp add:is_aligned_neg_mask_eq)
-   apply (clarsimp) *)
- (*  apply (erule disjE)
+   apply (clarsimp simp:get_free_ref_def)
+   apply (erule disjE)
     apply (drule_tac x= "cs!0" in bspec)
      subgoal by clarsimp
     subgoal by simp
-   apply (clarsimp simp:cte_wp_at_caps_of_state ex_cte_cap_wp_to_def)
+   apply (clarsimp simp: cte_wp_at_caps_of_state ex_cte_cap_wp_to_def)
    apply (rule_tac x=aa in exI,rule exI,rule exI)
    apply (rule conjI, assumption)
-    by (clarsimp simp:diminished_def is_cap_simps mask_cap_def
-      cap_rights_update_def , simp split:cap.splits )
-qed*)
-sorry
+    apply (clarsimp simp: diminished_def is_cap_simps mask_cap_def
+                          cap_rights_update_def,
+              simp split: cap.splits )
+   done
 qed
 
 lemma asid_bits_ge_0:
@@ -262,7 +257,7 @@ lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]:
 
 lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
   "\<lbrace>\<lambda>s. descendants_range_in {ptr .. ptr+2^sz - 1} cref s \<and> pspace_no_overlap_range_cover ptr sz s \<and> invs s
-  \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2^ sz\<rbrace>
+  \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr \<and> cap_is_device c = dev) cref s \<and> idx \<le> 2^ sz\<rbrace>
   set_cap (cap.UntypedCap dev ptr sz idx) cref
  \<lbrace>\<lambda>rv s. invs s\<rbrace>"
   apply (rule hoare_name_pre_state)
@@ -276,10 +271,16 @@ lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
     set_cap_irq_handlers cap_table_at_lift_valid set_cap_typ_at
     set_untyped_cap_refs_respects_device_simple)
   apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps)
+  apply (intro conjI, clarsimp)
+        apply (rule ext, clarsimp simp:is_cap_simps)
+       apply (clarsimp split:cap.splits simp:is_cap_simps appropriate_cte_cap_def)
       apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD])
        apply clarsimp
       apply (clarsimp simp:is_cap_simps ex_cte_cap_wp_to_def appropriate_cte_cap_def cte_wp_at_caps_of_state)
      apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def)
+    apply (simp add:valid_irq_node_def)
+   apply (clarsimp simp:valid_irq_node_def)
+  apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def)
   apply (case_tac cap)
    apply (simp_all add:vs_cap_ref_def table_cap_ref_def)
   apply (rename_tac arch_cap)
@@ -289,8 +290,8 @@ lemma set_untyped_cap_invs_simple[Untyped_AI_assms]:
               valid_refs_def simp del:split_paired_All)
   apply (drule_tac x = cref in spec)
   apply (clarsimp simp:cte_wp_at_caps_of_state)
-(*  apply fastforce *)
-  sorry
+  apply fastforce
+  done
 
 
 lemma pbfs_atleast_pageBits':
@@ -409,7 +410,7 @@ lemma store_pde_weaken:
             split: Structures_A.kernel_object.splits arch_kernel_obj.splits)
   done
 
-(* ARMHYP not needed anymore? *)
+(* ARMHYP not needed anymore?
 lemma store_pde_nonempty_table:
   "\<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table {}) r s)
            \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow>
@@ -421,7 +422,7 @@ lemma store_pde_nonempty_table:
   apply (wp get_object_wp)
   apply (clarsimp simp: obj_at_def nonempty_table_def a_type_def)
   apply (clarsimp simp add: empty_table_def vspace_bits_defs)
-  sorry
+  done *)
 
 (*
 lemma valid_arch_state_global_pd: (* ARMHYP restate? *)
diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
index fc8ad974f..6c655ed7e 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy
@@ -840,13 +840,9 @@ lemma perform_page_directory_valid_pdpt[wp]:
    apply (wp | wpc | simp)+
   done
 
-lemma perform_vcpu_valid_pdpt[wp]:
-  "\<lbrace>valid_pdpt_objs and valid_vcpu_invocation vi\<rbrace>
-      perform_vcpu_invocation vi \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>"
-  apply (simp add: perform_vcpu_invocation_def split_def)
-  apply (rule hoare_pre)
-   apply (wp | wpc | simp)+
-  sorry
+crunch valid_pdpt_objs[wp]: perform_vcpu_invocation "valid_pdpt_objs"
+  (ignore: delete_objects wp: delete_objects_valid_pdpt static_imp_wp)
+
 
 lemma perform_invocation_valid_pdpt[wp]:
   "\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs
@@ -1190,22 +1186,22 @@ lemma create_mapping_entries_safe[wp]:
   apply (drule_tac x = "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3)"
     in spec)
    apply (simp add: vspace_bits_defs)
-(*  apply (clarsimp simp:not_less[symmetric] split:list.splits)
+  apply (clarsimp simp:not_less[symmetric] vspace_bits_defs split:list.splits)
   apply (clarsimp simp:page_inv_entries_pre_def
     Let_def upto_enum_step_def upto_enum_def)
   apply (subst (asm) upto_0_to_n2)
    apply simp
-  apply (clarsimp simp:not_less[symmetric])
+  apply (clarsimp simp:not_less[symmetric] vspace_bits_defs)
   apply (subgoal_tac
     "(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 3))
-     = pde.PageTablePDE x xa xb)
-     \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3)) 7")
-   apply clarsimp
+     = pde.PageTablePDE x)
+     \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3)) 7")
+   apply (clarsimp simp: vspace_bits_defs)
    apply (subgoal_tac "
-     ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3) \<le>
-     ptrFromPAddr x + ((vptr >> 12) && 0xFF << 3) + 0x3C")
-    apply (clarsimp simp:not_less[symmetric])
-   apply (erule is_aligned_no_wrap')
+     ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) \<le>
+     ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) + 0x78")
+    apply (clarsimp simp:not_less[symmetric] vspace_bits_defs word_1FF_is_mask[symmetric])
+  (* apply (erule is_aligned_no_wrap')
    apply simp
   apply clarsimp
   apply (rule aligned_add_aligned)
diff --git a/proof/invariant-abstract/BCorres2_AI.thy b/proof/invariant-abstract/BCorres2_AI.thy
index d61daf1aa..0e591d45c 100644
--- a/proof/invariant-abstract/BCorres2_AI.thy
+++ b/proof/invariant-abstract/BCorres2_AI.thy
@@ -87,11 +87,6 @@ lemma valid_ntfn_trans_state[simp]: "valid_ntfn a (trans_state g s) = valid_ntfn
   apply (simp add: valid_ntfn_def split: ntfn.splits)
   done
 
-lemma [simp]: "\<forall>x5. b = ArchObj x5 \<longrightarrow>
-         wellformed_arch_obj x5 (trans_state g s) =
-         wellformed_arch_obj x5 s"
-sorry
-
 lemma valid_obj_trans_state[simp]: "valid_obj a b (trans_state g s) = valid_obj a b s"
   apply (simp add: valid_obj_def
               split: kernel_object.splits option.splits)
diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy
index 34ae6467c..8b02035e4 100644
--- a/proof/invariant-abstract/CNodeInv_AI.thy
+++ b/proof/invariant-abstract/CNodeInv_AI.thy
@@ -1765,6 +1765,9 @@ lemma cap_swap_fd_reply_masters[wp]:
 crunch refs_of[wp]: cap_swap "\<lambda>s. P (state_refs_of s)"
   (ignore: set_cap simp: state_refs_of_pspaceI)
 
+crunch hyp_refs_of[wp]: cap_swap "\<lambda>s. P (state_hyp_refs_of s)"
+  (ignore: set_cap simp: state_refs_of_pspaceI)
+
 crunch cur_tcb[wp]: cap_swap "cur_tcb"
 
 
@@ -1853,12 +1856,15 @@ lemma cap_swap_irq_handlers[wp]:
   done
 
 
+crunch vspace_objs [wp]: cap_swap "valid_vspace_objs"
+
+(*
 crunch arch_objs [wp]: cap_swap "valid_arch_objs"
 
 crunch arch_objs [wp]: cap_move "valid_arch_objs"
 
 crunch arch_objs [wp]: empty_slot "valid_arch_objs"
-
+*)
 
 context CNodeInv_AI begin
 
@@ -1976,7 +1982,7 @@ lemma cap_swap_invs[wp]:
                 simp del: split_paired_Ex split_paired_All
          | rule conjI
          | fastforce dest!: valid_reply_caps_of_stateD)+
-  sorry
+  done
 
 lemma cap_swap_fd_invs[wp]:
   "\<And>a b.
diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy
index 348df4c59..3a18c9f7b 100644
--- a/proof/invariant-abstract/CSpace_AI.thy
+++ b/proof/invariant-abstract/CSpace_AI.thy
@@ -4639,7 +4639,7 @@ crunch empty_table_at[wp]: setup_reply_master "obj_at (empty_table S) p"
 
 
 lemmas setup_reply_master_valid_vso_at[wp]
-    = ARM.valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
+    = valid_vso_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
 
 
 crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings"
diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy
index e634e31b6..723be88d6 100644
--- a/proof/invariant-abstract/Finalise_AI.thy
+++ b/proof/invariant-abstract/Finalise_AI.thy
@@ -36,7 +36,6 @@ requalify_facts
   no_irq_clearMemory
   valid_global_refsD
   valid_global_refsD2
-  prepare_thread_delete_def (* FIXME *)
 
 end
 
@@ -123,7 +122,7 @@ locale Finalise_AI_1 =
           \<and> cte_wp_at (op = cap) sl s \<and> valid_objs s \<and> sym_refs (state_refs_of s)
           \<and> (cap_irqs cap \<noteq> {} \<longrightarrow> if_unsafe_then_cap s \<and> valid_global_refs s)
           \<and> (is_arch_cap cap \<longrightarrow> pspace_aligned s \<and>
-                                 valid_arch_objs s \<and>
+                                 valid_vspace_objs s \<and>
                                  valid_arch_state s)\<rbrace>
        finalise_cap cap x
      \<lbrace>\<lambda>rv s. replaceable s sl (fst rv) cap\<rbrace>"
@@ -826,19 +825,19 @@ lemma cap_delete_one_cte_wp_at_preserved:
 interpretation delete_one_pre
   by (unfold_locales, wp cap_delete_one_cte_wp_at_preserved)
 
-
 lemma (in Finalise_AI_1) finalise_cap_equal_cap[wp]:
   "\<lbrace>cte_wp_at (op = cap) sl :: 'a state \<Rightarrow> bool\<rbrace>
      finalise_cap cap fin
    \<lbrace>\<lambda>rv. cte_wp_at (op = cap) sl\<rbrace>"
   apply (cases cap, simp_all split del: if_split)
     apply (wp suspend_cte_wp_at_preserved
-                 deleting_irq_handler_cte_preserved
+                 deleting_irq_handler_cte_preserved prepare_thread_delete_cte_wp_at
                  hoare_drop_imp thread_set_cte_wp_at_trivial
-               | clarsimp simp: can_fast_finalise_def unbind_maybe_notification_def unbind_notification_def
+               | clarsimp simp: can_fast_finalise_def unbind_maybe_notification_def
+                                unbind_notification_def
                                 tcb_cap_cases_def
                | wpc )+
-  sorry
+  done
 
 lemma emptyable_lift:
   assumes typ_at: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at T t s)\<rbrace>"
@@ -1082,12 +1081,13 @@ lemma (in Finalise_AI_3) finalise_cap_cte_cap_to[wp]:
   "\<lbrace>ex_cte_cap_wp_to P sl :: 'a state \<Rightarrow> bool\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>"
   apply (cases cap, simp_all add: ex_cte_cap_wp_to_def split del: if_split)
        apply (wp hoare_vcg_ex_lift hoare_drop_imps
+                 prepare_thread_delete_cte_preserved_irqn
                  deleting_irq_handler_cte_preserved_irqn
                  prepare_thread_delete_cte_preserved_irqn
                  | simp
                  | clarsimp simp: can_fast_finalise_def
                            split: cap.split_asm | wpc)+
-  sorry
+  done
 
 lemma (in Finalise_AI_3) finalise_cap_zombie_cap[wp]:
   "\<lbrace>cte_wp_at (\<lambda>cp. is_zombie cp \<and> P cp) sl :: 'a state \<Rightarrow> bool\<rbrace>
@@ -1096,7 +1096,7 @@ lemma (in Finalise_AI_3) finalise_cap_zombie_cap[wp]:
   apply (cases cap, simp_all split del: if_split)
        apply (wp deleting_irq_handler_cte_preserved
                | clarsimp simp: is_cap_simps can_fast_finalise_def)+
-  sorry
+  done
 
 lemma fast_finalise_st_tcb_at:
   "\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace>
diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy
index 974d5f1e6..56824bbf0 100644
--- a/proof/invariant-abstract/Invariants_AI.thy
+++ b/proof/invariant-abstract/Invariants_AI.thy
@@ -95,7 +95,8 @@ requalify_facts
   hyp_refs_of_live
   hyp_refs_of_live_obj
   tcb_arch_ref_simps
-
+  wellformed_arch_pspace
+  wellformed_arch_typ
 end
 
 lemmas [intro!] =  idle_global acap_rights_update_id
@@ -1572,11 +1573,6 @@ lemma valid_cap_pspaceI:
             simp: obj_range_def valid_untyped_def pred_tcb_at_def
            split: option.split sum.split)
 
-(* FIXME move to ArchInvariants and requalify *)
-lemma wellformed_arch_pspace: "\<And>ao. \<lbrakk>wellformed_arch_obj ao s; kheap s = kheap s'\<rbrakk>
-          \<Longrightarrow> wellformed_arch_obj ao s'"
-sorry
-
 (* FIXME-NTFN: ugly proof *)
 lemma valid_obj_pspaceI:
   "\<lbrakk> valid_obj ptr obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_obj ptr obj s'"
@@ -2204,12 +2200,6 @@ lemma valid_ntfn_typ:
   apply (rule hoare_vcg_conj_lift [OF hoare_vcg_prop], simp add: P)
   done
 
-(* FIXME move to ArchInvariants and requalify *)
-lemma wellformed_arch_typ:
-   "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> \<Longrightarrow>
-        \<lbrace>wellformed_arch_obj ao\<rbrace> f \<lbrace>\<lambda>rv. wellformed_arch_obj ao\<rbrace>"
-sorry
-
 lemma valid_obj_typ:
   assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
   shows      "\<lbrace>\<lambda>s. valid_obj p ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_obj p ob s\<rbrace>"
diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy
index d381924fb..d97cbefd6 100644
--- a/proof/invariant-abstract/IpcCancel_AI.thy
+++ b/proof/invariant-abstract/IpcCancel_AI.thy
@@ -1002,10 +1002,10 @@ lemma unbind_notification_invs:
   apply (rule hoare_seq_ext [OF _ get_ntfn_sp])
   apply (wp valid_irq_node_typ set_ntfn_valid_objs
        | clarsimp)+
-          defer 4
+          defer 5
           apply (auto elim!: obj_at_weakenE obj_at_valid_objsE if_live_then_nonz_capD2
-                       simp: valid_ntfn_set_bound_None is_ntfn valid_obj_def)[10]
-(*  apply (clarsimp simp: if_split) *)
+                       simp: valid_ntfn_set_bound_None is_ntfn valid_obj_def)[9]
+  apply (clarsimp simp: if_split)
   apply (rule delta_sym_refs, assumption)
    apply (fastforce simp: obj_at_def is_tcb
                    dest!: pred_tcb_at_tcb_at ko_at_state_refs_ofD
@@ -1017,12 +1017,12 @@ lemma unbind_notification_invs:
    apply (fastforce simp: obj_at_def is_tcb ntfn_q_refs_no_NTFNBound tcb_at_no_ntfn_bound refs_of_rev
                           tcb_ntfn_is_bound_def
                    dest!: pred_tcb_at_tcb_at bound_tcb_at_state_refs_ofD)
-(*  apply (subst (asm) ko_at_state_refs_ofD, assumption)
+  apply (subst (asm) ko_at_state_refs_ofD, assumption)
   apply (fastforce simp: ntfn_bound_refs_def obj_at_def ntfn_q_refs_no_TCBBound
                   elim!: pred_tcb_weakenE
-                  dest!: bound_tcb_bound_notification_at refs_in_ntfn_bound_refs symreftype_inverse' 
-                  split: option.splits) *)
-  sorry
+                  dest!: bound_tcb_bound_notification_at refs_in_ntfn_bound_refs symreftype_inverse'
+                  split: option.splits)
+  done
 
 
 crunch bound_tcb_at[wp]: cancel_all_signals "bound_tcb_at P t"
@@ -1147,7 +1147,7 @@ crunch cte_wp_at[wp]: cancel_all_signals "cte_wp_at P p"
 
 lemma cancel_badged_sends_filterM_helper':
   "\<forall>ys.
-   \<lbrace>\<lambda>s. all_invs_but_sym_refs s \<and> distinct (xs @ ys) \<and> ep_at epptr s
+   \<lbrace>\<lambda>s. all_invs_but_sym_refs s  \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s
            \<and> ex_nonz_cap_to epptr s
            \<and> sym_refs ((state_refs_of s) (epptr := ((set (xs @ ys)) \<times> {EPSend})))
            \<and> (\<forall>x \<in> set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace>
@@ -1159,7 +1159,7 @@ lemma cancel_badged_sends_filterM_helper':
                       od
                       else return True
                    od) xs
-   \<lbrace>\<lambda>rv s. all_invs_but_sym_refs s
+   \<lbrace>\<lambda>rv s. all_invs_but_sym_refs s \<and> sym_refs (state_hyp_refs_of s)
             \<and> ep_at epptr s \<and> (\<forall>x \<in> set (xs @ ys). tcb_at x s)
             \<and> ex_nonz_cap_to epptr s
             \<and> (\<forall>y \<in> set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})
@@ -1182,6 +1182,7 @@ lemma cancel_badged_sends_filterM_helper':
   apply clarsimp
   apply (thin_tac "ep_at epptr s" for s)
   apply (thin_tac "tcb_at x s" for x s)
+  apply (thin_tac "sym_refs (state_hyp_refs_of s)" for s)
   apply (frule singleton_eqD, clarify, drule state_refs_of_elemD)
   apply (frule(1) if_live_then_nonz_capD, rule refs_of_live, clarsimp)
   apply (clarsimp simp: st_tcb_at_refs_of_rev)
@@ -1218,8 +1219,9 @@ lemma cancel_badged_sends_invs[wp]:
                 cong: list.case_cong)
      apply (rule hoare_strengthen_post,
             rule cancel_badged_sends_filterM_helper[where epptr=epptr])
+
      apply (auto intro:obj_at_weakenE)[1]
-(*    apply (wp valid_irq_node_typ)
+    apply (wp valid_irq_node_typ)
    apply (clarsimp simp: valid_ep_def conj_comms)
    apply (subst obj_at_weakenE[where P'=is_ep], assumption)
     apply (clarsimp simp: is_ep_def)
@@ -1232,8 +1234,8 @@ lemma cancel_badged_sends_invs[wp]:
    apply (drule st_tcb_at_state_refs_ofD)
    apply (clarsimp simp only: cancel_badged_sends_invs_helper Un_iff, clarsimp)
    apply (simp add: set_eq_subset)
-  apply wpsimp *)
-  sorry
+  apply wpsimp
+  done
 
 
 lemma real_cte_emptyable_strg:
diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy
index b597e1a7f..fad863a9d 100644
--- a/proof/invariant-abstract/Ipc_AI.thy
+++ b/proof/invariant-abstract/Ipc_AI.thy
@@ -214,6 +214,11 @@ locale Ipc_AI =
       \<lbrace>cte_wp_at P p :: 'state_ext state \<Rightarrow> bool\<rbrace>
         do_fault_transfer x t label msg
       \<lbrace> \<lambda>rv. cte_wp_at P p \<rbrace>"
+  assumes transfer_caps_loop_valid_vspace_objs:
+  "\<And>ep buffer n caps slots mi.
+    \<lbrace>valid_vspace_objs::'state_ext state \<Rightarrow> bool\<rbrace>
+      transfer_caps_loop ep buffer n caps slots mi
+    \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
   assumes arch_get_sanitise_register_info_typ_at[wp]:
   "\<And> P T p t.
       \<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace>
@@ -1045,11 +1050,19 @@ lemma transfer_caps_loop_invs[wp]:
           \<and> transfer_caps_srcs caps s\<rbrace> 
       transfer_caps_loop ep buffer n caps slots mi
     \<lbrace>\<lambda>rv. invs\<rbrace>"
-  unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ)
+  unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ transfer_caps_loop_valid_vspace_objs)
 
 end
 
 (* FIXME: move *)
+crunch valid_vspace_objs [wp]: set_extra_badge valid_vspace_objs
+
+crunch vspace_objs [wp]: set_untyped_cap_as_full "valid_vspace_objs"
+  (wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
+
+crunch vspace_objs [wp]: cap_insert "valid_vspace_objs"
+  (wp: crunch_wps simp: crunch_simps ignore: set_object set_cap)
+
 lemma zipWith_append2:
   "length ys + 1 < n \<Longrightarrow>
    zipWith f [0 ..< n] (ys @ [y]) = zipWith f [0 ..< n] ys @ [f (length ys) y]"
@@ -1588,10 +1601,10 @@ crunch irq_handlers[wp]: do_ipc_transfer "valid_irq_handlers :: 'state_ext state
   (wp: crunch_wps hoare_vcg_const_Ball_lift simp: zipWithM_x_mapM crunch_simps ball_conj_distrib )
 
 crunch vspace_objs[wp]: transfer_caps_loop "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
-  (wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
+  (wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
 
 crunch vspace_objs[wp]: do_ipc_transfer "valid_vspace_objs :: 'state_ext state \<Rightarrow> bool"
-  (wp: crunch_wps simp: zipWithM_x_mapM crunch_simps)
+  (wp: crunch_wps transfer_caps_loop_valid_vspace_objs simp: zipWithM_x_mapM crunch_simps)
 
 crunch arch_caps[wp]: do_ipc_transfer "valid_arch_caps :: 'state_ext state \<Rightarrow> bool"
   (wp: crunch_wps hoare_vcg_const_Ball_lift transfer_caps_loop_valid_arch_caps
@@ -2584,9 +2597,10 @@ lemma ri_invs':
        conj_comms tcb_at_cte_at_2)
      apply (erule delta_sym_refs)
       apply (clarsimp split: if_split_asm)
-       apply ((clarsimp simp: pred_tcb_at_def2 tcb_bound_refs_def2 is_tcb
+     apply (clarsimp split: if_split_asm if_split) (* FIXME *)
+       apply ((fastforce simp: pred_tcb_at_def2 tcb_bound_refs_def2 is_tcb
                        dest!: symreftype_inverse')+)[3]
-(*    apply (rule conjI)
+    apply (rule conjI)
      apply (clarsimp simp: pred_tcb_at_def2 tcb_bound_refs_def2
                      split: if_split_asm)
      apply (simp add: set_eq_subset)
@@ -2623,7 +2637,7 @@ lemma ri_invs':
   apply (rule hoare_pre)
    apply (wp get_ntfn_wp | wpc | clarsimp)+
   apply (clarsimp simp: pred_tcb_at_tcb_at)
-  done *) sorry
+  done
 
 lemmas ri_invs[wp]
   = ri_invs'[where Q=\<top>,simplified hoare_post_taut, OF TrueI TrueI TrueI,simplified]
diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy
index 65eabd4f2..5bc2acaa4 100644
--- a/proof/invariant-abstract/KHeap_AI.thy
+++ b/proof/invariant-abstract/KHeap_AI.thy
@@ -23,7 +23,6 @@ requalify_consts
 
 requalify_facts
   pspace_in_kernel_window_atyp_lift
-(*  valid_arch_objs_lift_weak *)
   valid_vspace_objs_lift_weak
   vs_lookup_vspace_obj_at_lift
   vs_lookup_pages_vspace_obj_at_lift
@@ -32,7 +31,7 @@ requalify_facts
   valid_kernel_mappings_lift
   equal_kernel_mappings_lift
   valid_machine_state_lift
-(*  valid_ao_at_lift_aobj_at*)
+  valid_vso_at_lift
   valid_vso_at_lift_aobj_at
   valid_arch_state_lift_aobj_at
   in_user_frame_lift
@@ -50,6 +49,12 @@ requalify_facts
   pspace_respects_region_cong
   cap_is_device_obj_is_device
   storeWord_device_state_inv
+
+  state_hyp_refs_of_ep_update
+  state_hyp_refs_of_ntfn_update
+  state_hyp_refs_of_tcb_state_update
+  state_hyp_refs_of_tcb_bound_ntfn_update
+  wellformed_arch_obj_same_type
 end
 
 lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device
@@ -76,14 +81,6 @@ lemma get_tcb_rev:
   "kheap s p = Some (TCB t)\<Longrightarrow> get_tcb p s = Some t"
   by (clarsimp simp:get_tcb_def)
 
-(* moved to KHeapPre_AI
-lemma get_tcb_SomeD: "get_tcb t s = Some v \<Longrightarrow> kheap s t = Some (TCB v)"
-  apply (cases "kheap s t"; simp add: get_tcb_def)
-  apply (rename_tac obj)
-  apply (case_tac obj; simp)
-  done
-*)
-
 lemma get_tcb_obj_atE[elim!]:
   "\<lbrakk> get_tcb t s = Some tcb; get_tcb t s = Some tcb \<Longrightarrow> P (TCB tcb) \<rbrakk> \<Longrightarrow> obj_at P t s"
   by (clarsimp dest!: get_tcb_SomeD simp: obj_at_def)
@@ -106,13 +103,6 @@ lemma pspace_aligned_obj_update:
   done
 
 
-lemma typ_at_same_type:
-  assumes "typ_at T p s" "a_type k = a_type ko" "kheap s p' = Some ko"
-  shows "typ_at T p (s\<lparr>kheap := kheap s(p' \<mapsto> k)\<rparr>)"
-  using assms 
-  by (clarsimp simp: obj_at_def)
-
-
 lemma cte_at_same_type:
   "\<lbrakk>cte_at t s; a_type k = a_type ko; kheap s p = Some ko\<rbrakk>
   \<Longrightarrow> cte_at t (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
@@ -133,29 +123,6 @@ lemma untyped_same_type:
   unfolding valid_untyped_def
   by (clarsimp simp: obj_range_def obj_bits_T)
 
-lemma hoare_to_pure_kheap_upd:
-  assumes hoare[rule_format]:
-    "\<And>f. (\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace>
-      f \<lbrace>\<lambda>r s. P (typ_at (AArch T) p s)\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
-  assumes typ_eq: "a_type k = a_type ko"
-  assumes valid: "P (s :: ('z :: state_ext) state)"
-  assumes at: "ko_at ko p s"
-  shows "P (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
-  apply (rule use_valid[where f="
-      do
-        s' <- get;
-        assert (s' = s);
-        (modify (\<lambda>s. s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>));
-        return undefined
-      od", OF _ hoare valid])
-  apply (fastforce simp add: simpler_modify_def get_def bind_def
-                             assert_def return_def[abs_def] fail_def)[1]
-  apply wp
-  apply (insert typ_eq at)
-  apply clarsimp
-  apply (erule_tac P=P in rsubst)
-  by (auto simp add: obj_at_def a_type_def split: kernel_object.splits if_splits)
-
 lemma valid_cap_same_type:
   "\<lbrakk> s \<turnstile> cap; a_type k = a_type ko; kheap s p = Some ko \<rbrakk> 
   \<Longrightarrow> s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr> \<turnstile> cap"
@@ -167,6 +134,11 @@ lemma valid_cap_same_type:
       assumption, auto)
 
 
+lemma wellformed_arch_obj_same_type:
+  "\<lbrakk> wellformed_arch_obj obj s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
+   \<Longrightarrow> wellformed_arch_obj obj (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
+oops
+
 lemma valid_obj_same_type:
   "\<lbrakk> valid_obj p' obj s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
    \<Longrightarrow> valid_obj p' obj (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
@@ -187,33 +159,9 @@ lemma valid_obj_same_type:
    apply (auto elim: typ_at_same_type
                    simp: tcb_at_typ
                   split: Structures_A.ntfn.splits option.splits)
-
-  apply (simp add: valid_obj_def "ARM.wellformed_arch_obj_def"
-                 ARM_A.arch_kernel_obj.distinct
-                 ARM_A.arch_kernel_obj.inject
-            split: ARM_A.arch_kernel_obj.splits)
-  apply (rename_tac v)
-  apply (case_tac "ARM_A.vcpu_tcb v"; simp add: ARM.valid_vcpu_def)
-  apply (drule typ_at_same_type[rotated]; assumption)
-done
-
-lemma valid_arch_obj_same_type:
-  "\<lbrakk>valid_arch_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
-  \<Longrightarrow> valid_arch_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> ko')\<rparr>)"
-  apply (induction ao rule: ARM_A.arch_kernel_obj.induct;
-         clarsimp simp: ARM.valid_arch_obj.simps typ_at_same_type)
-    apply (rule hoare_to_pure_kheap_upd; assumption?)
-      apply (rule ARM.valid_pte_lift, assumption)
-     apply blast
-    apply (simp add: obj_at_def)
-   apply (rule hoare_to_pure_kheap_upd; assumption?)
-     apply (rule ARM.valid_pde_lift, assumption)
-    apply blast
-   apply (simp add: obj_at_def)
-  apply (rename_tac v)
-  apply (case_tac "ARM_A.vcpu_tcb v"; simp add: ARM.valid_vcpu_def)
-  apply (drule typ_at_same_type[rotated]; assumption)
-done
+  apply (clarsimp simp add: valid_obj_def)
+  apply (auto intro: wellformed_arch_obj_same_type)
+  done
 
 lemma valid_vspace_obj_same_type:
   "\<lbrakk>valid_vspace_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
@@ -543,16 +491,15 @@ lemma set_ep_refs_of[wp]:
 
 
 lemma set_ep_hyp_refs_of[wp]:
- "\<lbrace>\<lambda>s. P (ARM.state_hyp_refs_of s)\<rbrace>
+ "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
     set_endpoint ep val
-  \<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
+  \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
   apply (simp add: set_endpoint_def set_object_def)
   apply (rule hoare_seq_ext [OF _ get_object_sp])
-  apply wp
-  apply clarsimp
-  apply (drule_tac ARM.ko_at_state_hyp_refs_ofD)
-  apply (case_tac obj; clarsimp elim!: rsubst[where P=P])
-  apply (rule all_ext; clarsimp simp: ARM.state_hyp_refs_of_def ARM.hyp_refs_of_simps ARM.hyp_refs_of_def)
+  apply (wp, clarsimp)
+  apply (subst state_hyp_refs_of_ep_update[of ep _ val, simplified fun_upd_def])
+  apply (case_tac obj; clarsimp simp: typ_at_eq_kheap_obj obj_at_def)
+  apply assumption
   done
 
 
@@ -815,18 +762,18 @@ lemma set_ntfn_refs_of[wp]:
   done
 
 lemma set_ntfn_hyp_refs_of[wp]: (* ARMHYP *)
-  "\<lbrace>\<lambda>s. P ((ARM.state_hyp_refs_of s))\<rbrace>
+  "\<lbrace>\<lambda>s. P ((state_hyp_refs_of s))\<rbrace>
      set_notification ntfnptr ntfn
-   \<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
+   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
   apply (simp add: set_notification_def set_object_def)
   apply (rule hoare_seq_ext [OF _ get_object_sp])
-  apply wp
-  apply clarsimp
-  apply (drule_tac ARM.ko_at_state_hyp_refs_ofD)
-  apply (case_tac obj; clarsimp elim!: rsubst[where P=P])
-  apply (rule all_ext; clarsimp simp: ARM.state_hyp_refs_of_def ARM.hyp_refs_of_simps ARM.hyp_refs_of_def)
+  apply (wp, clarsimp)
+  apply (subst state_hyp_refs_of_ntfn_update[of ntfnptr _ ntfn, simplified fun_upd_def])
+  apply (case_tac obj; clarsimp simp: typ_at_eq_kheap_obj obj_at_def)
+  apply assumption
   done
 
+
 lemma set_ntfn_cur_tcb[wp]:
   "\<lbrace>cur_tcb\<rbrace> set_notification ntfn v \<lbrace>\<lambda>rv. cur_tcb\<rbrace>"
   apply (simp add: set_notification_def set_object_def)
@@ -1302,16 +1249,6 @@ lemma set_object_non_pagetable:
   apply (clarsimp simp: obj_at_def)
   by (rule vspace_obj_predE)
 
-(*
-lemma set_object_arch_objs_non_arch:
-  "\<lbrace>valid_arch_objs and K (non_arch_obj ko) and obj_at non_arch_obj p\<rbrace>
-  set_object p ko
-  \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
-  apply (rule assert_pre)
-  apply (rule hoare_pre)
-  apply (rule valid_arch_objs_lift_weak)
-  apply (wp set_object_non_arch | clarsimp)+
-  done *)
 
 lemma set_object_vspace_objs_non_pagetable:
   "\<lbrace>valid_vspace_objs and K (non_vspace_obj ko) and obj_at non_vspace_obj p\<rbrace>
@@ -1376,10 +1313,7 @@ by (rule valid_kernel_mappings_lift, wp vsobj_at)
 
 lemma equal_kernel_mappings[wp]: "\<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>_. equal_kernel_mappings\<rbrace>"
 by (rule equal_kernel_mappings_lift, wp vsobj_at)
-(*
-lemma valid_ao_at[wp]:"\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>_. valid_ao_at p\<rbrace>"
-by (rule valid_ao_at_lift_aobj_at; wp aobj_at; simp)
-*)
+
 lemma valid_vso_at[wp]:"\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>_. valid_vso_at p\<rbrace>"
 by (rule valid_vso_at_lift_aobj_at; wp vsobj_at; simp)
 
@@ -1662,7 +1596,7 @@ lemma set_ntfn_minor_invs:
      set_notification ptr val
    \<lbrace>\<lambda>rv. invs\<rbrace>"
   apply (simp add: invs_def valid_state_def valid_pspace_def)
-  apply_trace (rule hoare_pre,
+  apply (rule hoare_pre,
          wp_trace set_ntfn_valid_objs valid_irq_node_typ
             valid_irq_handlers_lift)
   apply (clarsimp elim!: rsubst[where P=sym_refs]
@@ -1725,9 +1659,9 @@ lemma dmo_refs_of[wp]:
 
 
 lemma dmo_hyp_refs_of[wp]:
-  "\<lbrace>\<lambda>s. P (ARM.state_hyp_refs_of s)\<rbrace>
+  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
      do_machine_op oper
-   \<lbrace>\<lambda>rv s. P (ARM.state_hyp_refs_of s)\<rbrace>"
+   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
   apply (simp add: do_machine_op_def split_def)
   apply wp
   apply (clarsimp elim!: state_hyp_refs_of_pspaceI)
diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy
index fc92d0a6f..4acb6184e 100644
--- a/proof/invariant-abstract/TcbAcc_AI.thy
+++ b/proof/invariant-abstract/TcbAcc_AI.thy
@@ -1173,16 +1173,21 @@ lemma sts_refs_of[wp]:
   apply (simp add: get_tcb_def sts_refs_of_helper)
   done
 
+lemma kheap_Some_state_hyp_refs_ofD:
+  "kheap s p = Some ko \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko"
+  by (rule ko_at_state_hyp_refs_ofD; simp add: obj_at_def)
+
 (* FIXME should be able to prove this in the generic context *)
 lemma sts_hyp_refs_of[wp]:
   "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
     set_thread_state t st
    \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
   apply (simp add: set_thread_state_def set_object_def)
-  apply (wp, simp, wp)
-  apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD)
-  apply (rule state_hyp_refs_update[symmetric])
-  sorry
+  apply (wp | simp del: fun_upd_apply)+
+  apply (clarsimp simp: get_tcb_def split: option.splits kernel_object.splits
+                  simp del: fun_upd_apply)
+  apply (subst state_hyp_refs_of_tcb_state_update; assumption)
+  done
 
 lemma sbn_refs_of_helper: "
           {r. (r \<in> tcb_st_refs_of ts \<or>
@@ -1204,17 +1209,18 @@ lemma sbn_refs_of[wp]:
   apply (auto simp: get_tcb_def sbn_refs_of_helper)
   done
 
+
 (* FIXME the same as the above FIXME *)
 lemma sbn_hyp_refs_of[wp]:
   "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
     set_bound_notification t ntfn
    \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>"
   apply (simp add: set_bound_notification_def set_object_def)
-  apply (wp, simp)
-  apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD
-                 intro!: ext)
-  apply (auto simp: get_tcb_def)
-  sorry
+  apply (wp, simp del: fun_upd_apply)
+  apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD simp del: fun_upd_apply
+                  intro!: ext)
+  apply (subst state_hyp_refs_of_tcb_bound_ntfn_update; auto simp: get_tcb_def)
+  done
 
 lemma set_thread_state_thread_set:
   "set_thread_state p st = (do thread_set (tcb_state_update (\<lambda>_. st)) p;
diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy
index d5af4ebcf..f3168c695 100644
--- a/proof/invariant-abstract/Untyped_AI.thy
+++ b/proof/invariant-abstract/Untyped_AI.thy
@@ -3847,7 +3847,7 @@ lemma invoke_untyp_invs':
                    distinct_tuple_helper
                    init_arch_objects_wps
                    init_arch_objects_nonempty_table
-              | wp_once retype_region_ret_folded_general)
+              | wp_once retype_region_ret_folded_general)+
         apply ((wp hoare_vcg_const_imp_lift hoare_drop_imp
                    retype_region_invs_extras[where sz = sz]
                    retype_region_aligned_for_init[where sz = sz]
@@ -3858,7 +3858,7 @@ lemma invoke_untyp_invs':
                          distinct_map_fst_zip
             | simp add: ptr_base
             | wp_once retype_region_ret_folded_general)+)[1]
- (*      apply (clarsimp simp:conj_comms,simp cong:conj_cong)
+       apply (clarsimp simp:conj_comms,simp cong:conj_cong)
        apply (simp add:ball_conj_distrib conj_comms)
        apply (strengthen invs_mdb invs_valid_pspace
                 caps_region_kernel_window_imp[where p="(cref, oref)"]
@@ -3943,8 +3943,7 @@ lemma invoke_untyp_invs':
       apply (frule untyped_mdb_descendants_range, clarsimp+,
         erule invoke_untyped_proofs.descendants_range, simp_all+)[1]
       apply (simp add: untyped_range_def atLeastatMost_subset_iff word_and_le2)
-*)
-      sorry
+      done
 qed
 
 lemmas invoke_untyp_invs[wp] =