diff --git a/proof/refine/RISCV64/ArchAcc_R.thy b/proof/refine/RISCV64/ArchAcc_R.thy
index 949ff7d76..8572aa620 100644
--- a/proof/refine/RISCV64/ArchAcc_R.thy
+++ b/proof/refine/RISCV64/ArchAcc_R.thy
@@ -515,7 +515,7 @@ lemma lookupPTSlotFromLevel_inv:
    apply (subst lookupPTSlotFromLevel.simps)
    apply (wpsimp simp: pteAtIndex_def wp: getPTE_wp)
   apply (subst lookupPTSlotFromLevel.simps)
-  apply (wpsimp simp: pteAtIndex_def wp: getPTE_wp|assumption)+
+  apply (wpsimp simp: pteAtIndex_def checkPTAt_def wp: getPTE_wp|assumption)+
   done
 
 declare lookupPTSlotFromLevel_inv[wp]
@@ -524,11 +524,11 @@ lemma lookupPTFromLevel_inv[wp]:
   "lookupPTFromLevel level pt vptr target_pt \<lbrace>P\<rbrace>"
 proof (induct level arbitrary: pt)
   case 0 show ?case
-    by (subst lookupPTFromLevel.simps, simp, wp)
+    by (subst lookupPTFromLevel.simps, simp add: checkPTAt_def, wp)
 next
   case (Suc level)
   show ?case
-    by (subst lookupPTFromLevel.simps, simp)
+    by (subst lookupPTFromLevel.simps, simp add: checkPTAt_def)
        (wpsimp wp: Suc getPTE_wp simp: pteAtIndex_def)
 qed
 
@@ -630,7 +630,13 @@ next
   show ?case
     apply (subst pt_lookup_slot_from_level_rec)
     apply (simp add: lookupPTSlotFromLevel.simps Let_def obind_comp_dist if_comp_dist
-                     gets_the_if_distrib)
+                     gets_the_if_distrib checkPTAt_def)
+    apply (rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
+     apply clarsimp
+     apply (rule page_table_at_cross; assumption?)
+      apply (drule (5) valid_vspace_objs_strongD)
+      apply (clarsimp simp: pt_at_eq in_omonad)
+     apply (simp add: state_relation_def)
     apply (rule corres_guard_imp, rule corres_split[where r'=pte_relation'])
          apply (rule corres_if3)
            apply (rename_tac pte pte', case_tac pte; (simp add: isPageTablePTE_def))
@@ -690,7 +696,13 @@ proof (induct level arbitrary: level' pt pt')
   case 0
   then show ?case
     apply (subst lookupPTFromLevel.simps, subst pt_lookup_from_level_simps)
-    apply (clarsimp simp: lookup_failure_map_def)
+    apply (clarsimp simp: checkPTAt_def liftE_bindE)
+    apply (rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
+     apply clarsimp
+     apply (rule page_table_at_cross; assumption?)
+      apply (drule vs_lookup_table_pt_at; simp?)
+     apply (simp add: state_relation_def)
+    apply (simp add: lookup_failure_map_def)
     done
 next
   case (minus level)
@@ -745,6 +757,13 @@ next
   from minus.prems
   show ?case
     apply (subst lookupPTFromLevel.simps, subst pt_lookup_from_level_simps)
+    apply (clarsimp simp: checkPTAt_def)
+    apply (subst liftE_bindE,
+           rule corres_stateAssert_implied[where P'="\<lambda>_. True", simplified, rotated])
+     apply clarsimp
+     apply (rule page_table_at_cross; assumption?)
+      apply (drule vs_lookup_table_pt_at; simp?)
+     apply (simp add: state_relation_def)
     apply (simp add: unlessE_whenE not_less)
     apply (rule corres_initial_splitE[where r'=dc])
        apply (corressimp simp: lookup_failure_map_def)
diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy
index 66d5eddc3..b226b89e1 100644
--- a/proof/refine/RISCV64/EmptyFail_H.thy
+++ b/proof/refine/RISCV64/EmptyFail_H.thy
@@ -150,7 +150,7 @@ proof (induct level arbitrary: pt)
 next
   case (Suc level)
   then show ?case
-    by (subst lookupPTSlotFromLevel.simps) (wpsimp simp: pteAtIndex_def)
+    by (subst lookupPTSlotFromLevel.simps) (wpsimp simp: checkPTAt_def pteAtIndex_def)
 qed
 
 lemma empty_fail_arch_cap_exhausted:
diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy
index d61c2a666..46c6f802d 100644
--- a/proof/refine/RISCV64/Retype_R.thy
+++ b/proof/refine/RISCV64/Retype_R.thy
@@ -12,6 +12,10 @@ theory Retype_R
 imports VSpace_R
 begin
 
+(* FIXME RISCV: move way up somewhere *)
+text \<open>To ensure that the proof state is in a certain case of a case distinction:\<close>
+method in_case for x::'a = match premises in "t = x" for t \<Rightarrow> succeed
+
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 definition
@@ -2191,28 +2195,29 @@ proof -
       using cover
       apply (clarsimp simp: RISCV64_H.toAPIType_def APIType_capBits_def
                       split: RISCV64_H.object_type.splits)
-            \<comment> \<open>SmallPageObject\<close>
+         apply (in_case "HugePageObject")
          apply wp
           apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
           apply (wp createObjects_aligned2 createObjects_nonzero'
-                    cwo_ret'[where bs=0, simplified]
+                    cwo_ret'[where bs="ptTranslationBits + ptTranslationBits", simplified]
                  | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
          apply (simp add:pageBits_def ptr word_bits_def)
-        \<comment> \<open>LargePageObject\<close>
+        apply (in_case "SmallPageObject")
         apply wp
          apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
          apply (wp createObjects_aligned2 createObjects_nonzero'
-                   cwo_ret'[where bs=ptTranslationBits, simplified]
+                   cwo_ret'[where bs=0, simplified]
                 | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
         apply (simp add:pageBits_def ptr word_bits_def)
-       \<comment> \<open>HugePageObject\<close>
+       apply (in_case \<open>LargePageObject\<close>)
+
        apply wp
         apply (simp add: valid_cap'_def capAligned_def n_less_word_bits ball_conj_distrib)
         apply (wp createObjects_aligned2 createObjects_nonzero'
-                  cwo_ret'[where bs="ptTranslationBits + ptTranslationBits", simplified]
+                  cwo_ret'[where bs=ptTranslationBits, simplified]
                | simp add: objBits_if_dev pageBits_def ptr range_cover_n_wb)+
        apply (simp add:pageBits_def ptr word_bits_def)
-      \<comment> \<open>PageTableObject\<close>
+      apply (in_case \<open>PageTableObject\<close>)
       apply wp
        apply (simp add: valid_cap'_def capAligned_def n_less_word_bits)
        apply (rule hoare_chain)
@@ -2231,7 +2236,7 @@ proof -
         apply (rule ucast_less[where 'b="pt_index_len" and 'a="machine_word_len", simplified])
        apply simp
       apply clarsimp
-   done
+      done
   next
     case (Some a) thus ?thesis
     proof(cases a)
@@ -5181,7 +5186,7 @@ lemma corres_retype_region_createNewCaps:
       apply (clarsimp simp: list_all2_same list_all2_map1 list_all2_map2 objBits_simps
                             allRights_def APIType_map2_def
                       split del: if_split)
-     \<comment> \<open>SmallPageObject\<close>
+     apply (in_case \<open>HugePageObject\<close>)
      apply (subst retype_region2_extra_ext_trivial)
       apply (simp add: APIType_map2_def)
      apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@@ -5191,13 +5196,13 @@ lemma corres_retype_region_createNewCaps:
         apply (rule corres_retype_update_gsI;
                clarsimp simp: obj_bits_api_def3 APIType_map2_def objBits_simps ext
                               default_object_def default_arch_object_def makeObjectKO_def
-                              data_page_relation_retype
+                              data_page_relation_retype bit_simps
                        elim!: range_cover.aligned;
                assumption)
        apply fastforce+
-     apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
-                      list_all2_map1 list_all2_map2 list_all2_same)
-    \<comment> \<open>LargePageObject\<close>
+   apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
+                    list_all2_map1 list_all2_map2 list_all2_same)
+    apply (in_case \<open>SmallPageObject\<close>)
     apply (subst retype_region2_extra_ext_trivial)
      apply (simp add: APIType_map2_def)
     apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@@ -5211,9 +5216,9 @@ lemma corres_retype_region_createNewCaps:
                       elim!: range_cover.aligned;
               assumption)
       apply fastforce+
-    apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
-                     list_all2_map1 list_all2_map2 list_all2_same)
-   \<comment> \<open>HugePageObject\<close>
+     apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
+                      list_all2_map1 list_all2_map2 list_all2_same)
+   apply (in_case \<open>LargePageObject\<close>)
    apply (subst retype_region2_extra_ext_trivial)
     apply (simp add: APIType_map2_def)
    apply (simp add: corres_liftM2_simp[unfolded liftM_def] split del: if_split)
@@ -5223,13 +5228,13 @@ lemma corres_retype_region_createNewCaps:
       apply (rule corres_retype_update_gsI;
              clarsimp simp: obj_bits_api_def3 APIType_map2_def objBits_simps ext
                             default_object_def default_arch_object_def makeObjectKO_def
-                            data_page_relation_retype bit_simps
+                            data_page_relation_retype
                      elim!: range_cover.aligned;
              assumption)
      apply fastforce+
-   apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
-                    list_all2_map1 list_all2_map2 list_all2_same)
-  \<comment> \<open>PageTable\<close>
+    apply (simp add: APIType_map2_def arch_default_cap_def vm_read_write_def vmrights_map_def
+                     list_all2_map1 list_all2_map2 list_all2_same)
+  apply (in_case \<open>PageTableObject\<close>)
   apply (subst retype_region2_extra_ext_trivial)
    apply (simp add: APIType_map2_def)
   apply (simp_all add: corres_liftM2_simp[unfolded liftM_def])
@@ -5244,7 +5249,7 @@ lemma corres_retype_region_createNewCaps:
     apply (clarsimp simp: list_all2_map1 list_all2_map2 list_all2_same
                           APIType_map2_def arch_default_cap_def)
    apply fastforce+
- done
+  done
 
 end
 end
diff --git a/proof/refine/RISCV64/Untyped_R.thy b/proof/refine/RISCV64/Untyped_R.thy
index 305313118..335cb4ec4 100644
--- a/proof/refine/RISCV64/Untyped_R.thy
+++ b/proof/refine/RISCV64/Untyped_R.thy
@@ -4625,6 +4625,16 @@ lemma (in range_cover) funky_aligned:
   apply simp
   done
 
+(* FIXME RISCV: move to Corres_UL *)
+lemma corres_assert_gen_asm_cross:
+  "\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A;
+     A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
+  \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (Q and Q') f (assert A >>= g)"
+  by (metis corres_assert_assume corres_cases corres_name_pre)
+
+defs canonicalAddressAssert_def:
+  "canonicalAddressAssert p \<equiv> RISCV64.canonical_address p"
+
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 lemma inv_untyped_corres':
@@ -4863,6 +4873,11 @@ lemma inv_untyped_corres':
     have sz_limit[simp]: "sz \<le> maxUntypedSizeBits"
       using vc' unfolding valid_cap'_def by clarsimp
 
+    have canonical_ptr[simp]: "canonical_address ptr"
+      using ptr_cn sz_limit
+      unfolding canonical_address_range maxUntypedSizeBits_def canonical_bit_def
+      by word_bitwise (simp add: word_size)
+
     note set_cap_free_index_invs_spec = set_free_index_invs[where cap = "cap.UntypedCap
         dev (ptr && ~~ mask sz) sz (if reset then 0 else idx)"
       ,unfolded free_index_update_def free_index_of_def,simplified]
@@ -4887,6 +4902,7 @@ lemma inv_untyped_corres':
                 sz (if reset then 0 else idx)" in corres_gen_asm)
           apply (rule corres_add_noop_lhs)
           apply (rule corres_split_nor[OF _ cNodeNoOverlap return_wp stateAssert_wp])
+          apply (clarsimp simp: canonicalAddressAssert_def)
           apply (rule corres_split[OF _ updateFreeIndex_corres,rotated])
               apply (simp add:isCap_simps)+
              apply (clarsimp simp:getFreeIndex_def bits_of_def shiftL_nat shiftl_t2n