diff --git a/proof/crefine/Arch_C.thy b/proof/crefine/Arch_C.thy
index e40e8062a..da20a8b1d 100644
--- a/proof/crefine/Arch_C.thy
+++ b/proof/crefine/Arch_C.thy
@@ -564,7 +564,7 @@ shows
    apply simp+
   apply (clarsimp simp:typ_heap_simps' region_is_bytes'_def[where sz=0])
   apply (frule ccte_relation_ccap_relation)
-  apply (clarsimp simp: cap_get_tag_isCap)
+  apply (clarsimp simp: cap_get_tag_isCap hrs_htd_update)
   apply (clarsimp simp: hrs_htd_update_def split_def 
                          pageBits_def 
                    split: split_if)
@@ -575,18 +575,17 @@ shows
     apply (simp add: ghost_assertion_data_get_gs_clear_region[unfolded o_def])
    apply (drule valid_global_refsD_with_objSize, clarsimp)+
    apply (clarsimp simp: isCap_simps dest!: ccte_relation_ccap_relation)
-  apply (cut_tac ptr=frame and bits=12 and s="globals_update (t_hrs_'_update (hrs_htd_update
-               (typ_region_bytes frame 12))) s'" in typ_region_bytes_actually_is_bytes)
+  apply (cut_tac ptr=frame and bits=12
+    and htd="typ_region_bytes frame 12 (hrs_htd (t_hrs_' (globals s')))" in typ_region_bytes_actually_is_bytes)
    apply (simp add: hrs_htd_update)
-  apply clarsimp
+  apply (clarsimp simp: region_actually_is_bytes'_def[where len=0])
   apply (intro conjI)
        apply (clarsimp elim!:is_aligned_weaken)
       apply (simp add:is_aligned_def)
-     apply (erule is_aligned_no_wrap',simp)
-    apply (drule region_actually_is_bytes_dom_s[OF _ order_refl])
-    apply (simp add: hrs_htd_update_def split_def)
-   apply (clarsimp simp: region_actually_is_bytes_def hrs_htd_update)
-   apply (simp add: hrs_htd_def hrs_htd_update_def split_def)
+     apply (simp add: hrs_htd_def)
+    apply (erule is_aligned_no_wrap',simp)
+   apply (drule region_actually_is_bytes_dom_s[OF _ order_refl])
+   apply (simp add: hrs_htd_def split_def)
   apply (clarsimp simp: ccap_relation_def)
   apply (clarsimp simp: cap_asid_pool_cap_lift)
   apply (clarsimp simp: cap_to_H_def)
diff --git a/proof/crefine/CSpace_C.thy b/proof/crefine/CSpace_C.thy
index 33cebc1f7..a916a779a 100644
--- a/proof/crefine/CSpace_C.thy
+++ b/proof/crefine/CSpace_C.thy
@@ -2332,6 +2332,12 @@ lemma region_is_bytes_subset:
     \<Longrightarrow> region_is_bytes' ptr' sz' htd"
   by (auto simp: region_is_bytes'_def)
 
+lemma region_actually_is_bytes_subset:
+  "region_actually_is_bytes' ptr sz htd
+    \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
+    \<Longrightarrow> region_actually_is_bytes' ptr' sz' htd"
+  by (auto simp: region_actually_is_bytes'_def)
+
 lemma intvl_both_le:
   "\<lbrakk> a \<le> x; unat x + y \<le> unat a + b \<rbrakk>
     \<Longrightarrow>  {x ..+ y} \<le> {a ..+ b}"
@@ -2420,7 +2426,7 @@ lemma ctes_of_untyped_zero_rf_sr_case:
       untyped_ranges_zero' s \<rbrakk>
     \<Longrightarrow> case untypedZeroRange (cteCap cte)
                of None \<Rightarrow> True
-    | Some (start, end) \<Rightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
+    | Some (start, end) \<Rightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
   by (simp split: option.split add: ctes_of_untyped_zero_rf_sr)
 
 lemma gsUntypedZeroRanges_update_helper:
@@ -2449,7 +2455,7 @@ lemma updateTrackedFreeIndex_noop_ccorres:
               \<and> idx \<le> 2 ^ capBlockSize cap
               \<and> (capFreeIndex cap \<le> idx \<or> cap' = cap)) o cteCap) slot
           and valid_objs' and untyped_ranges_zero')
-      {s. \<not> capIsDevice cap' \<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
+      {s. \<not> capIsDevice cap' \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx) (capFreeIndex cap' - idx) s} hs
       (updateTrackedFreeIndex slot idx) Skip"
   (is "ccorres dc xfdc ?P ?P' _ _ _")
   apply (simp add: updateTrackedFreeIndex_def getSlotCap_def)
@@ -2478,16 +2484,16 @@ lemma updateTrackedFreeIndex_noop_ccorres:
      apply clarsimp
      apply (thin_tac "\<not> capIsDevice cap' \<longrightarrow> P" for P)
      apply (clarsimp split: option.split_asm)
-     apply (subst region_is_bytes_subset, simp+)
+     apply (subst region_actually_is_bytes_subset, simp+)
      apply (subst heap_list_is_zero_mono2, simp+)
     apply (frule untypedZeroRange_idx_backward_helper[where idx=idx],
       simp+)
     apply (clarsimp simp: isCap_simps valid_cap_simps')
     apply (clarsimp split: option.split_asm)
      apply (clarsimp dest!: untypedZeroRange_not_device)
-     apply (subst region_is_bytes_subset, simp+)
+     apply (subst region_actually_is_bytes_subset, simp+)
      apply (subst heap_list_is_zero_mono2, simp+)
-    apply (simp add: region_is_bytes'_def heap_list_zero_Ball_intvl)
+    apply (simp add: region_actually_is_bytes'_def heap_list_zero_Ball_intvl)
     apply (clarsimp dest!: untypedZeroRange_not_device)
     apply blast
    apply (clarsimp simp: cte_wp_at_ctes_of)
@@ -2503,7 +2509,7 @@ lemma updateTrackedFreeIndex_forward_noop_ccorres:
   apply (rule ccorres_name_pre)
    apply (rule ccorres_guard_imp2,
      rule_tac cap'="cteCap (the (ctes_of s slot))" in updateTrackedFreeIndex_noop_ccorres)
-  apply (clarsimp simp: cte_wp_at_ctes_of region_is_bytes'_def)
+  apply (clarsimp simp: cte_wp_at_ctes_of region_actually_is_bytes'_def)
   done
 
 lemma clearUntypedFreeIndex_noop_ccorres:
diff --git a/proof/crefine/Detype_C.thy b/proof/crefine/Detype_C.thy
index 974ebd20d..7651d439f 100644
--- a/proof/crefine/Detype_C.thy
+++ b/proof/crefine/Detype_C.thy
@@ -1618,7 +1618,7 @@ lemma zero_ranges_are_zero_typ_region_bytes:
     \<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs)"
   apply (clarsimp simp: zero_ranges_are_zero_def)
   apply (drule(1) bspec)
-  apply (clarsimp simp: region_is_bytes'_def typ_region_bytes_def hrs_htd_update)
+  apply (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def hrs_htd_update)
   done
 
 lemma deleteObjects_ccorres':
diff --git a/proof/crefine/Invoke_C.thy b/proof/crefine/Invoke_C.thy
index ca274dc81..9ba6d4c22 100644
--- a/proof/crefine/Invoke_C.thy
+++ b/proof/crefine/Invoke_C.thy
@@ -1942,6 +1942,21 @@ lemma eq_UntypedCap_helper:
     \<Longrightarrow> cap = UntypedCap dev ptr sz idx"
   by (clarsimp simp: isCap_simps)
 
+lemma byte_regions_unmodified_actually_heap_list:
+  "byte_regions_unmodified hrs hrs'
+    \<Longrightarrow> region_actually_is_bytes' p' n' htd
+    \<Longrightarrow> htd = (hrs_htd hrs)
+    \<Longrightarrow> heap_list (hrs_mem hrs) n p = v
+    \<Longrightarrow> {p ..+ n} \<subseteq> {p' ..+ n'}
+    \<Longrightarrow> heap_list (hrs_mem hrs') n p = v"
+  apply (erule trans[rotated], rule heap_list_h_eq2)
+  apply (simp add: byte_regions_unmodified_def region_actually_is_bytes_def)
+  apply (drule_tac x=x in spec)
+  apply (drule_tac x=x in bspec)
+   apply blast
+  apply (clarsimp split: split_if_asm)
+  done
+
 lemma resetUntypedCap_ccorres:
   notes upt.simps[simp del] Collect_const[simp del] replicate_numeral[simp del]
   shows
@@ -2021,7 +2036,7 @@ lemma resetUntypedCap_ccorres:
           apply (simp add: guard_is_UNIV_def)
          apply wp
         apply simp
-        apply (vcg exspec=cleanCacheRange_PoU_modifies)
+        apply (vcg exspec=cleanCacheRange_PoU_preserves_bytes)
        apply (rule_tac P="reset_chunk_bits \<le> capBlockSize (cteCap cte)
              \<and> of_nat (capFreeIndex (cteCap cte)) - 1
                  < (2 ^ capBlockSize (cteCap cte) :: addr)"
@@ -2115,7 +2130,7 @@ lemma resetUntypedCap_ccorres:
                 apply (simp add: guard_is_UNIV_def)
                apply (wp hoare_vcg_ex_lift doMachineOp_psp_no_overlap)
               apply clarsimp
-              apply (vcg exspec=cleanCacheRange_PoU_modifies)
+              apply (vcg exspec=cleanCacheRange_PoU_preserves_bytes)
              apply clarify
              apply (rule conjI)
               apply (clarsimp simp: invs_valid_objs' cte_wp_at_ctes_of
@@ -2158,21 +2173,26 @@ lemma resetUntypedCap_ccorres:
                                is_aligned_mult_triv2[THEN is_aligned_weaken]
                                region_actually_is_bytes_subset_t_hrs[mk_strg I E]
                            | simp)+
-             apply (clarsimp simp: capAligned_def
+             apply (clarsimp simp: capAligned_def imp_conjL
                                    aligned_offset_non_zero
                                    is_aligned_add_multI conj_comms
                                    is_aligned_mask_out_add_eq_sub[OF is_aligned_weaken])
-             apply (strengthen region_is_bytes_subset[OF region_actually_is_bytes, mk_strg I E]
+             apply (strengthen region_actually_is_bytes_subset[mk_strg I E]
                     heap_list_is_zero_mono[OF heap_list_update_eq]
                     order_trans [OF intvl_start_le
                           aligned_intvl_offset_subset[where sz'=reset_chunk_bits]]
-                | simp add: is_aligned_mult_triv2)+
+                    byte_regions_unmodified_actually_heap_list[mk_strg I E E]
+                | simp add: is_aligned_mult_triv2 hrs_mem_update)+
              apply (simp add: unat_sub word_le_nat_alt unat_sub[OF word_and_le2]
                               mask_out_sub_mask word_and_le2
                               unat_of_nat32[OF order_le_less_trans, rotated,
                                 OF power_strict_increasing])
              apply (case_tac idx')
               (* must be contradictory *)
+              apply clarsimp
+              apply (simp add: is_aligned_def addr_card_def card_word
+                               reset_chunk_bits_def)
+              apply clarsimp
               apply (simp add: is_aligned_def addr_card_def card_word
                                reset_chunk_bits_def)
              apply (simp add: unat_of_nat32[OF order_le_less_trans, rotated,
@@ -2181,9 +2201,9 @@ lemma resetUntypedCap_ccorres:
                               unat_mod unat_of_nat mod_mod_cancel)
              apply (strengthen nat_le_Suc_less_imp[OF mod_less_divisor, THEN order_trans])
              apply (simp add: is_aligned_def addr_card_def card_word)
+             apply clarsimp
 
-            apply clarsimp
-            apply (rule conseqPre, vcg exspec=cleanCacheRange_PoU_modifies
+            apply (rule conseqPre, vcg exspec=cleanCacheRange_PoU_preserves_bytes
               exspec=preemptionPoint_modifies)
             apply (clarsimp simp: in_set_conv_nth isCap_simps
                                   length_upto_enum_step upto_enum_step_nth
@@ -2318,7 +2338,10 @@ lemma resetUntypedCap_ccorres:
                     region_is_bytes_typ_region_bytes
                     intvl_start_le is_aligned_power2
                     heap_list_is_zero_mono[OF heap_list_update_eq]
-    | simp add: unat_of_nat)+
+                    byte_regions_unmodified_actually_heap_list[OF _ _ refl, mk_strg I E]
+                    typ_region_bytes_actually_is_bytes[OF refl]
+                    region_actually_is_bytes_subset[OF typ_region_bytes_actually_is_bytes[OF refl]]
+    | simp add: unat_of_nat imp_conjL hrs_mem_update hrs_htd_update)+
   apply (clarsimp simp: order_trans[OF power_increasing[where a=2]]
                         addr_card_def card_word
                         is_aligned_weaken from_bool_0)
@@ -2331,7 +2354,7 @@ lemma ccorres_cross_retype_zero_bytes_over_guard:
         ((\<lambda>s. invs' s
       \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx
           \<and> idx \<le> unat (ptr && mask sz)) p s) and P')
-      {s'. (\<not> dev \<longrightarrow> region_is_zero_bytes ptr
+      {s'. (\<not> dev \<longrightarrow> region_actually_is_zero_bytes ptr
             (num_ret * 2 ^ APIType_capBits newType userSize) s')
          \<and> (\<exists>cte cte' idx. cslift s' (cte_Ptr p) = Some cte'
                  \<and> ccte_relation cte cte' \<and> cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx)
@@ -2342,7 +2365,7 @@ lemma ccorres_cross_retype_zero_bytes_over_guard:
   apply (frule(2) rf_sr_cte_relation)
   apply (case_tac dev)
    apply fastforce
-  apply (frule(1) retype_offs_region_is_zero_bytes, (simp | clarsimp)+)
+  apply (frule(1) retype_offs_region_actually_is_zero_bytes, (simp | clarsimp)+)
   apply fastforce
   done
 
@@ -2637,13 +2660,15 @@ lemma invokeUntyped_Retype_ccorres:
         apply (clarsimp simp: ccHoarePost_def hrs_mem_update
                               object_type_from_H_bound
                               typ_heap_simps' word_sle_def
-                              word_of_nat_less zero_bytes_heap_update)
+                              word_of_nat_less zero_bytes_heap_update
+                              region_actually_is_bytes)
         apply (frule ccte_relation_ccap_relation)
         apply (cut_tac vui)
         apply (clarsimp simp: cap_get_tag_isCap getFreeIndex_def
                               cte_wp_at_ctes_of shiftL_nat
                        split: split_if)
         apply (simp add: mask_out_sub_mask field_simps region_is_bytes'_def)
+        apply (clarsimp elim!: region_actually_is_bytes_subset)
        apply (rule order_refl)
 
       apply (cut_tac misc us_misc' proofs us_misc bits_low
diff --git a/proof/crefine/Machine_C.thy b/proof/crefine/Machine_C.thy
index 4133fb96c..d6ec8d03d 100644
--- a/proof/crefine/Machine_C.thy
+++ b/proof/crefine/Machine_C.thy
@@ -74,6 +74,12 @@ assumes cleanByVA_PoU_ccorres:
            (doMachineOp (cleanByVA_PoU w1 w2))
            (Call cleanByVA_PoU_'proc)"
 
+assumes cleanByVA_PoU_preserves_kernel_bytes:
+ "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc
+      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
+         \<and> (\<forall>x. snd (hrs_htd (t_hrs_' (globals s)) x) 0 \<noteq> None
+             \<longrightarrow> hrs_mem (t_hrs_' (globals t)) x = hrs_mem (t_hrs_' (globals s)) x)}"
+
 assumes invalidateByVA_ccorres:
   "ccorres dc xfdc \<top> (\<lbrace>\<acute>vaddr = w1\<rbrace> \<inter> \<lbrace>\<acute>paddr = w2\<rbrace>) []
            (doMachineOp (invalidateByVA w1 w2))
diff --git a/proof/crefine/Recycle_C.thy b/proof/crefine/Recycle_C.thy
index ef2995b25..07b266986 100644
--- a/proof/crefine/Recycle_C.thy
+++ b/proof/crefine/Recycle_C.thy
@@ -1289,7 +1289,7 @@ lemma updateFreeIndex_ccorres:
            and untyped_ranges_zero'
            and (\<lambda>_. is_aligned (of_nat idx' :: word32) 4 \<and> idx' \<le> 2 ^ (capBlockSize cap')))
            {s. \<not> capIsDevice cap'
-               \<longrightarrow> region_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
+               \<longrightarrow> region_actually_is_zero_bytes (capPtr cap' + of_nat idx') (capFreeIndex cap' - idx') s} hs
            (updateFreeIndex srcSlot idx') c"
   (is "_ \<Longrightarrow> ccorres dc xfdc (valid_objs' and ?cte_wp_at' and _ and _) ?P' hs ?a c")
   apply (rule ccorres_gen_asm)
diff --git a/proof/crefine/Retype_C.thy b/proof/crefine/Retype_C.thy
index 812a9ebfe..10ac3a1c6 100644
--- a/proof/crefine/Retype_C.thy
+++ b/proof/crefine/Retype_C.thy
@@ -1497,11 +1497,11 @@ lemma region_is_bytes_typ_region_bytes:
   apply (simp add: subsetD split: split_if_asm)
   done
 
-lemma region_is_bytes_retyp_disjoint:
+lemma region_actually_is_bytes_retyp_disjoint:
   "{ptr ..+ sz} \<inter> {ptr_val (p :: 'a ptr)..+n * size_of TYPE('a :: mem_type)} = {}
-    \<Longrightarrow> region_is_bytes' ptr sz htd
-    \<Longrightarrow> region_is_bytes' ptr sz (ptr_retyps_gen n p arr htd)"
-  apply (clarsimp simp: region_is_bytes'_def del: impI)
+    \<Longrightarrow> region_actually_is_bytes' ptr sz htd
+    \<Longrightarrow> region_actually_is_bytes' ptr sz (ptr_retyps_gen n p arr htd)"
+  apply (clarsimp simp: region_actually_is_bytes'_def del: impI)
   apply (subst ptr_retyps_gen_out)
    apply blast
   apply simp
@@ -1524,7 +1524,7 @@ lemma zero_ranges_ptr_retyps:
   apply (clarsimp simp: zero_ranges_are_zero_def untyped_ranges_zero_inv_def
                         hrs_htd_update)
   apply (drule(1) bspec, clarsimp)
-  apply (rule region_is_bytes_retyp_disjoint, simp_all)
+  apply (rule region_actually_is_bytes_retyp_disjoint, simp_all)
   apply (clarsimp simp: map_comp_Some_iff cteCaps_of_def
                  elim!: ranE)
   apply (frule(1) ctes_of_valid')
@@ -2638,6 +2638,7 @@ definition
 where
   "byte_regions_unmodified hrs hrs' \<equiv> \<forall>x. (\<forall>n td b. snd (hrs_htd hrs x) n = Some (td, b)
         \<longrightarrow> td = typ_uinfo_t TYPE (word8))
+    \<longrightarrow> snd (hrs_htd hrs x) 0 \<noteq> None
     \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x"
 
 abbreviation
@@ -2736,7 +2737,7 @@ lemma mdb_node_ptr_set_mdbNext_preserves_bytes:
 lemma updateNewFreeIndex_noop_ccorres:
   "ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot)
       {s. (case untypedZeroRange cap of None \<Rightarrow> True
-          | Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)} hs
+          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)} hs
       (updateNewFreeIndex slot) Skip"
   (is "ccorres _ _ ?P ?P' hs _ _")
   apply (simp add: updateNewFreeIndex_def getSlotCap_def)
@@ -2765,19 +2766,19 @@ lemma updateNewFreeIndex_noop_ccorres:
 
 lemma byte_regions_unmodified_region_is_bytes:
   "byte_regions_unmodified hrs hrs'
-    \<Longrightarrow> region_is_bytes' y n (hrs_htd hrs)
+    \<Longrightarrow> region_actually_is_bytes' y n (hrs_htd hrs)
     \<Longrightarrow> x \<in> {y ..+ n}
     \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x"
-  apply (clarsimp simp: byte_regions_unmodified_def)
+  apply (clarsimp simp: byte_regions_unmodified_def imp_conjL[symmetric])
   apply (drule spec, erule mp)
-  apply (clarsimp simp: region_is_bytes'_def)
-  apply metis
+  apply (clarsimp simp: region_actually_is_bytes'_def)
+  apply (drule(1) bspec, simp split: split_if_asm)
   done
 
 lemma insertNewCap_ccorres1:
   "ccorres dc xfdc (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap)
      ({s. (case untypedZeroRange cap of None \<Rightarrow> True
-          | Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)}
+          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
        \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
        \<inter> {s. slot_' s = Ptr slot}) []
      (insertNewCap parent slot cap) 
@@ -2813,7 +2814,7 @@ lemma insertNewCap_ccorres1:
   apply (rule conjI)
    apply (clarsimp simp: cte_wp_at_ctes_of is_aligned_3_next)
   apply (clarsimp split: option.split)
-  apply (intro allI conjI impI; simp; clarsimp)
+  apply (intro allI conjI impI; simp; clarsimp simp: region_actually_is_bytes)
    apply (erule trans[OF heap_list_h_eq2, rotated])
    apply (rule byte_regions_unmodified_region_is_bytes)
       apply (erule byte_regions_unmodified_trans[rotated]
@@ -4693,34 +4694,18 @@ lemma rf_sr_htd_safe:
   "(s, s') \<in> rf_sr \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s')))"
   by (simp add: rf_sr_def cstate_relation_def Let_def)
 
-definition
-  "region_actually_is_bytes ptr len s
-    = (\<forall>x \<in> {ptr ..+ len}. hrs_htd (t_hrs_' (globals s)) x
-        = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]))"
-
-abbreviation
-  "region_actually_is_zero_bytes ptr len s
-    \<equiv> region_actually_is_bytes ptr len s
-        \<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) ptr len"
-
 lemma region_actually_is_bytes_dom_s:
-  "region_actually_is_bytes ptr len s
+  "region_actually_is_bytes' ptr len htd
     \<Longrightarrow> S \<subseteq> {ptr ..+ len}
-    \<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s)))"
-  apply (clarsimp simp: region_actually_is_bytes_def dom_s_def)
+    \<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s htd"
+  apply (clarsimp simp: region_actually_is_bytes'_def dom_s_def)
   apply fastforce
   done
 
-lemma region_actually_is_bytes:
-  "region_actually_is_bytes ptr len s
-    \<Longrightarrow> region_is_bytes ptr len s"
-  by (simp add: region_is_bytes'_def region_actually_is_bytes_def
-         split: split_if)
-
 lemma typ_region_bytes_actually_is_bytes:
-  "hrs_htd (t_hrs_' (globals s)) = typ_region_bytes ptr bits htd
-    \<Longrightarrow> region_actually_is_bytes ptr (2 ^ bits) s"
-  by (clarsimp simp: region_actually_is_bytes_def typ_region_bytes_def)
+  "htd = typ_region_bytes ptr bits htd'
+    \<Longrightarrow> region_actually_is_bytes' ptr (2 ^ bits) htd"
+  by (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def)
 
 (* FIXME: need a way to avoid overruling the parser on this, it's ugly *)
 lemma memzero_modifies:
@@ -7622,6 +7607,16 @@ lemma copyGlobalMappings_preserves_bytes:
     (simp_all add: h_t_valid_field)+)
   done
 
+lemma cleanByVA_PoU_preserves_bytes:
+  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc
+      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
+         \<and> byte_regions_unmodified' s t}"
+  apply (rule allI, rule conseqPost,
+    rule cleanByVA_PoU_preserves_kernel_bytes[rule_format])
+   apply simp_all
+  apply (clarsimp simp: byte_regions_unmodified_def)
+  done
+
 lemma cleanCacheRange_PoU_preserves_bytes:
   "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanCacheRange_PoU_'proc
       {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
@@ -7631,7 +7626,7 @@ lemma cleanCacheRange_PoU_preserves_bytes:
   apply (subst whileAnno_def[symmetric, where V=undefined
        and I="{t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
          \<and> byte_regions_unmodified' s t}" for s])
-  apply (rule conseqPre, vcg)
+  apply (rule conseqPre, vcg exspec=cleanByVA_PoU_preserves_bytes)
   apply (safe intro!: byte_regions_unmodified_hrs_mem_update
     elim!: byte_regions_unmodified_trans byte_regions_unmodified_trans[rotated],
     (simp_all add: h_t_valid_field)+)
@@ -7661,8 +7656,9 @@ lemma Arch_createObject_preserves_bytes:
   apply (safe intro!: ptr_retyp_d ptr_retyps_out)
   apply (simp_all add: object_type_from_H_def Kernel_C_defs APIType_capBits_def
     split: object_type.split_asm ArchTypes_H.apiobject_type.split_asm)
-  apply (rule byte_regions_unmodified_flip,
-    simp add: hrs_htd_update hrs_htd_update_canon)
+   apply (rule byte_regions_unmodified_flip, simp)
+  apply (rule byte_regions_unmodified_trans[rotated],
+    assumption, simp_all add: hrs_htd_update_canon hrs_htd_update)
   done
 
 lemma ptr_arr_retyps_eq_outside_dom:
@@ -7670,8 +7666,6 @@ lemma ptr_arr_retyps_eq_outside_dom:
     \<Longrightarrow> ptr_arr_retyps n p htd x = htd x"
   by (simp add: ptr_arr_retyps_def htd_update_list_same2)
 
-text {* NOTE: FIXME: need a way to show that
-  createObject will preserve a zero heap list. *}
 lemma createObject_preserves_bytes:
   "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call createObject_'proc
       {t. \<forall>nt. t_' s = object_type_from_H nt
@@ -7758,12 +7752,12 @@ lemma offset_intvl_first_chunk_subsets_unat:
   apply (simp add: word_le_nat_alt word_less_nat_alt unat_of_nat)
   done
 
-lemma retype_offs_region_is_zero_bytes:
+lemma retype_offs_region_actually_is_zero_bytes:
   "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s;
       cteCap cte = UntypedCap False (ptr &&~~ mask sz) sz idx;
       idx \<le> unat (ptr && mask sz);
       range_cover ptr sz (getObjectSize newType userSize) num_ret \<rbrakk>
-    \<Longrightarrow> region_is_zero_bytes ptr
+    \<Longrightarrow> region_actually_is_zero_bytes ptr
             (num_ret * 2 ^ APIType_capBits newType userSize) s'"
   using word_unat_mask_lt[where w=ptr and m=sz]
   apply -
@@ -7772,7 +7766,7 @@ lemma retype_offs_region_is_zero_bytes:
    apply (simp add: untypedZeroRange_def max_free_index_def word_size)
   apply clarify
   apply (strengthen heap_list_is_zero_mono2[mk_strg I E]
-      region_is_bytes_subset[mk_strg I E])
+      region_actually_is_bytes_subset[mk_strg I E])
   apply (simp add: getFreeRef_def word_size)
   apply (rule intvl_both_le)
    apply (rule order_trans, rule word_plus_mono_right, erule word_of_nat_le)
@@ -7815,7 +7809,7 @@ lemma insertNewCap_ccorres:
           and valid_objs' and valid_cap' cap)
      ({s. cap_get_tag (cap_' s) = scast cap_untyped_cap
          \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (cap_' s)))) of None \<Rightarrow> True
-          | Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) s)}
+          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
        \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
        \<inter> {s. slot_' s = Ptr slot}) []
      (insertNewCap parent slot cap) 
@@ -7826,18 +7820,19 @@ lemma insertNewCap_ccorres:
   apply (clarsimp simp: ccap_relation_def map_option_Some_eq2)
   apply (simp add: untypedZeroRange_def Let_def)
   done
-
+find_theorems untypedZeroRange
+term zero_ranges_are_zero
 lemma createObject_untyped_region_is_zero_bytes:
   "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s. let tp = (object_type_to_H (t_' s));
           sz = APIType_capBits tp (unat (userSize_' s))
       in (\<not> to_bool (deviceMemory_' s)
-              \<longrightarrow> region_is_zero_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s)
+              \<longrightarrow> region_actually_is_zero_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s)
           \<and> is_aligned (ptr_val (regionBase_' s)) sz
           \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> sz \<ge> 4)}
       Call createObject_'proc
    {t. cap_get_tag (ret__struct_cap_C_' t) = scast cap_untyped_cap
          \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True
-          | Some (a, b) \<Rightarrow> region_is_zero_bytes a (unat ((b + 1) - a)) t)}"
+          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) t)}"
   apply (rule allI, rule conseqPre, vcg exspec=copyGlobalMappings_modifies
       exspec=Arch_initContext_modifies
       exspec=cleanCacheRange_PoU_modifies)
@@ -7885,7 +7880,7 @@ shows  "ccorres dc xfdc
                                            isFrameType newType)
                     \<and> (unat num = length destSlots)
                     )))
-    ({s. (\<not> isdev \<longrightarrow> region_is_zero_bytes ptr
+    ({s. (\<not> isdev \<longrightarrow> region_actually_is_zero_bytes ptr
             (length destSlots * 2 ^ APIType_capBits newType userSize) s)}
            \<inter> {s. t_' s = object_type_from_H newType}
            \<inter> {s. parent_' s = cte_Ptr srcSlot}
@@ -7925,7 +7920,7 @@ shows  "ccorres dc xfdc
      apply simp
      apply (clarsimp simp: whileAnno_def)
      apply (rule ccorres_rel_imp)
-      apply (rule_tac Q="{s. \<not> isdev \<longrightarrow> region_is_zero_bytes
+      apply (rule_tac Q="{s. \<not> isdev \<longrightarrow> region_actually_is_zero_bytes
             (ptr + (i_' s << APIType_capBits newType userSize))
             (unat (num - i_' s) * 2 ^ APIType_capBits newType userSize) s}"
             in ccorres_zipWithM_x_while_genQ[where j=1, OF _ _ _ _ _ i_xf_for_sequence, simplified])
@@ -8051,21 +8046,17 @@ shows  "ccorres dc xfdc
               apply (simp add: unat_eq_def)
              apply (drule range_cover_sz')
              apply (simp add: unat_eq_def word_less_nat_alt)
-            apply clarsimp
-            apply (erule heap_list_is_zero_mono)
-            apply (subgoal_tac "unat (num - of_nat n) \<noteq> 0")
-             apply simp
-            apply (simp only: unat_eq_0, clarsimp simp: unat_of_nat)
-           apply (simp add: hrs_htd_update typ_region_bytes_actually_is_bytes)
+            apply (simp add: hrs_htd_update typ_region_bytes_actually_is_bytes)
+           apply clarsimp
+           apply (erule heap_list_is_zero_mono)
+           apply (subgoal_tac "unat (num - of_nat n) \<noteq> 0")
+            apply simp
+           apply (simp only: unat_eq_0, clarsimp simp: unat_of_nat)
           apply (frule range_cover_sz')
           apply (clarsimp simp: Let_def hrs_htd_update
                                 APIType_capBits_def[where ty="APIObjectType ArchTypes_H.apiobject_type.Untyped"])
           apply (subst is_aligned_add, erule range_cover.aligned)
            apply (simp add: is_aligned_shiftl)+
-          apply clarsimp
-          apply (rule region_is_bytes_typ_region_bytes)
-          apply simp
-         apply clarsimp
          apply (subst range_cover.unat_of_nat_n)
           apply (erule range_cover_le)
           subgoal by simp
@@ -8083,7 +8074,7 @@ shows  "ccorres dc xfdc
         apply clarsimp
         apply (rule context_conjI)
          apply (simp add: hrs_htd_update)
-         apply (simp add: region_is_bytes'_def, rule ballI)
+         apply (simp add: region_actually_is_bytes'_def, rule ballI)
          apply (drule bspec, erule(1) subsetD)
          apply (drule(1) orthD2)
          apply (simp add: Ball_def unat_eq_def typ_bytes_region_out)
diff --git a/proof/crefine/SR_lemmas_C.thy b/proof/crefine/SR_lemmas_C.thy
index 8d84ecb40..9483f228d 100644
--- a/proof/crefine/SR_lemmas_C.thy
+++ b/proof/crefine/SR_lemmas_C.thy
@@ -1686,6 +1686,12 @@ lemma region_is_bytes_disjoint:
   apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def)
   done
 
+lemma region_actually_is_bytes:
+  "region_actually_is_bytes' ptr len htd
+    \<Longrightarrow> region_is_bytes' ptr len htd"
+  by (simp add: region_is_bytes'_def region_actually_is_bytes'_def
+         split: split_if)
+
 lemma zero_ranges_are_zero_update[simp]:
   "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr)
     \<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)
@@ -1693,6 +1699,7 @@ lemma zero_ranges_are_zero_update[simp]:
         = zero_ranges_are_zero rs hrs"
   apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update
         intro!: ball_cong[OF refl] conj_cong[OF refl])
+  apply (drule region_actually_is_bytes)
   apply (drule(2) region_is_bytes_disjoint)
   apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute)
   done
@@ -2228,7 +2235,7 @@ lemma page_table_at_rf_sr:
 
 lemma gsUntypedZeroRanges_rf_sr:
   "\<lbrakk> (start, end) \<in> gsUntypedZeroRanges s; (s, s') \<in> rf_sr \<rbrakk>
-    \<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
+    \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                         zero_ranges_are_zero_def)
   apply (drule(1) bspec)
@@ -2239,7 +2246,7 @@ lemma ctes_of_untyped_zero_rf_sr:
   "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
       untyped_ranges_zero' s;
       untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk>
-    \<Longrightarrow> region_is_zero_bytes start (unat ((end + 1) - start)) s'"
+    \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'"
   apply (erule gsUntypedZeroRanges_rf_sr[rotated])
   apply (clarsimp simp: untyped_ranges_zero_inv_def)
   apply (rule_tac a=p in ranI)
diff --git a/proof/crefine/StateRelation_C.thy b/proof/crefine/StateRelation_C.thy
index 03bdd4246..db8072e74 100644
--- a/proof/crefine/StateRelation_C.thy
+++ b/proof/crefine/StateRelation_C.thy
@@ -696,11 +696,29 @@ abbreviation
   "region_is_zero_bytes ptr n x \<equiv> region_is_bytes ptr n x
       \<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr n"
 
+definition
+  region_actually_is_bytes' :: "addr \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"
+where
+  "region_actually_is_bytes' ptr len htd
+    = (\<forall>x \<in> {ptr ..+ len}. htd x
+        = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]))"
+
+abbreviation
+  "region_actually_is_bytes ptr len s
+    \<equiv> region_actually_is_bytes' ptr len (hrs_htd (t_hrs_' (globals s)))"
+
+lemmas region_actually_is_bytes_def = region_actually_is_bytes'_def
+
+abbreviation
+  "region_actually_is_zero_bytes ptr len s
+    \<equiv> region_actually_is_bytes ptr len s
+        \<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) ptr len"
+
 definition
   zero_ranges_are_zero
 where
   "zero_ranges_are_zero rs hrs
-    = (\<forall>(start, end) \<in> rs. region_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs)
+    = (\<forall>(start, end) \<in> rs. region_actually_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs)
         \<and> heap_list_is_zero (hrs_mem hrs) start (unat ((end + 1) - start)))"
 
 definition (in state_rel)
diff --git a/proof/crefine/StoreWord_C.thy b/proof/crefine/StoreWord_C.thy
index 95e4baf76..1a401ac0a 100644
--- a/proof/crefine/StoreWord_C.thy
+++ b/proof/crefine/StoreWord_C.thy
@@ -641,6 +641,7 @@ proof (intro allI impI)
     apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
                           heap_update_def
           intro!: ball_cong[OF refl] conj_cong[OF refl])
+    apply (drule region_actually_is_bytes)
     apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
      apply simp
     apply (subst heap_list_update_disjoint_same, simp_all)
@@ -949,6 +950,7 @@ proof (intro allI impI)
     apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update base_def
                           heap_update_def
           intro!: ball_cong[OF refl] conj_cong[OF refl])
+    apply (drule region_actually_is_bytes)
     apply (frule(1) region_is_bytes_disjoint[rotated 2, OF h_t_valid_clift])
      apply simp
     apply (subst heap_list_update_disjoint_same, simp_all)
diff --git a/proof/crefine/Syscall_C.thy b/proof/crefine/Syscall_C.thy
index 7c8df9099..84a95c015 100644
--- a/proof/crefine/Syscall_C.thy
+++ b/proof/crefine/Syscall_C.thy
@@ -1363,11 +1363,13 @@ lemma handleRecv_ccorres:
 
           apply (simp add: liftE_bind)
           apply (ctac)
+            apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in ccorres_cross_over_guard)
             apply (ctac add: receiveIPC_ccorres[unfolded dc_def])
 
            apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift)
-          apply clarsimp
-          apply (vcg exspec=deleteCallerCap_modifies)
+          apply (rule conseqPost[where Q'=UNIV and A'="{}"], vcg exspec=deleteCallerCap_modifies)
+           apply (clarsimp dest!: rf_sr_ksCurThread)
+          apply simp
          apply clarsimp
          apply (vcg exspec=handleFault_modifies)
 
@@ -1499,6 +1501,7 @@ lemma handleRecv_ccorres:
      apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies)
 
     apply wp
+   apply clarsimp
    apply vcg
   
   apply (clarsimp simp add: sch_act_sane_def)