diff --git a/spec/abstract/RISCV64/ArchVSpace_A.thy b/spec/abstract/RISCV64/ArchVSpace_A.thy
index 3be3adee1..913e52c30 100644
--- a/spec/abstract/RISCV64/ArchVSpace_A.thy
+++ b/spec/abstract/RISCV64/ArchVSpace_A.thy
@@ -95,7 +95,7 @@ definition set_vm_root :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
        ArchObjectCap (PageTableCap pt (Some (asid, _))) \<Rightarrow> doE
            pt' \<leftarrow> find_vspace_for_asid asid;
            whenE (pt \<noteq> pt') $ throwError InvalidRoot;
-           liftE $ do_machine_op $ setVSpaceRoot pt asid
+           liftE $ do_machine_op $ setVSpaceRoot pt (ucast asid)
        odE
      | _ \<Rightarrow> throwError InvalidRoot) <catch>
     (\<lambda>_. do
@@ -129,7 +129,7 @@ definition delete_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::st
      | Some pool_ptr \<Rightarrow> do
          pool \<leftarrow> get_asid_pool pool_ptr;
          when (pool (asid_low_bits_of asid) = Some pt) $ do
-           do_machine_op $ hwASIDFlush asid;
+           do_machine_op $ hwASIDFlush (ucast asid);
            pool' \<leftarrow> return $ pool (asid_low_bits_of asid := None);
            set_asid_pool pool_ptr pool';
            tcb \<leftarrow> gets cur_thread;
diff --git a/spec/abstract/RISCV64/Machine_A.thy b/spec/abstract/RISCV64/Machine_A.thy
index 90141d8cc..f32bfd1c6 100644
--- a/spec/abstract/RISCV64/Machine_A.thy
+++ b/spec/abstract/RISCV64/Machine_A.thy
@@ -38,7 +38,7 @@ type_synonym asid_high_len   = 7
 type_synonym asid_high_index = "asid_high_len word"
 
 type_synonym asid_len        = 16
-type_synonym asid_rep_len    = machine_word_len
+type_synonym asid_rep_len    = asid_len
 type_synonym asid            = "asid_rep_len word"
 
 text \<open>