diff --git a/model/prelude.sail b/model/prelude.sail
index 8c03c58da..2b878591c 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -218,3 +218,21 @@ function log2(n) = {
   };
   result
 }
+
+/* This is a slightly arbitrary limit on the maximum number of bytes
+   in a memory access.  It helps to generate slightly better C code
+   because it means width argument can be fast native integer. It
+   would be even better if it could be <= 8 bytes so that data can
+   also be a 64-bit int but CHERI needs 128-bit accesses for
+   capabilities and SIMD / vector instructions will also need more.
+
+   The specific value does not matter (if it is >8) since anything up
+   to 2^64-1 will result in a native int being used for the width type.
+
+   4096 was chosen because it is a page size, and a reasonable maximum
+   for cbo.zero.
+   */
+type max_mem_access : Int = 4096
+
+// Type used for memory access widths. Zero byte accesses are not allowed.
+type mem_access_width = range(1, max_mem_access)
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 53bf8a83a..c19b9a23f 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -78,21 +78,6 @@ instantiation sail_mem_write with
      aborts, so just use unit here too */
   'abort = unit
 
-/* This is a slightly arbitrary limit on the maximum number of bytes
-   in a memory access.  It helps to generate slightly better C code
-   because it means width argument can be fast native integer. It
-   would be even better if it could be <= 8 bytes so that data can
-   also be a 64-bit int but CHERI needs 128-bit accesses for
-   capabilities and SIMD / vector instructions will also need more.
-
-   The specific value does not matter (if it is >8) since anything up
-   to 2^64-1 will result in a native int being used for the width type.
-
-   4096 was chosen because it is a page size, and a reasonable maximum
-   for cbo.zero.
-   */
-type max_mem_access : Int = 4096
-
 val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> bool
 
 function write_ram(wk, physaddr(addr), width, data, meta) = {
diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail
index 9a80a760f..b61a13054 100644
--- a/model/prelude_mem_metadata.sail
+++ b/model/prelude_mem_metadata.sail
@@ -14,8 +14,6 @@ type mem_meta = unit
 
 let default_meta : mem_meta = ()
 
-val __WriteRAM_Meta : forall 'n. (physaddrbits, int('n), mem_meta) -> unit
-function __WriteRAM_Meta(addr, width, meta) = ()
+function __WriteRAM_Meta(addr : physaddrbits, width : mem_access_width, meta : mem_meta) -> unit = ()
 
-val __ReadRAM_Meta  : forall 'n. (physaddrbits, int('n)) -> mem_meta
-function __ReadRAM_Meta(addr, width) = ()
+function __ReadRAM_Meta(addr : physaddrbits, width : mem_access_width) -> mem_meta = default_meta
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 991a9f280..05d2a85d4 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -54,7 +54,7 @@ type ext_data_addr_error = unit
 
 /* Default data addr is just base register + immediate offset (may be zero).
    Extensions might override and add additional checks. */
-function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access))
+function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : mem_access_width)
          -> Ext_DataAddr_Check(ext_data_addr_error) =
   let addr = virtaddr(X(base) + offset) in
   Ext_DataAddr_OK(addr)