Add mem_access_width type

* Add `mem_access_width` type. This will also be used for PMAs in future.
* Use `mem_access_width` type for `__Write/ReadRAM_Meta` instead of existential.
* Move `max_mem_access/width` to `prelude.sail`. This helps with compile dependency ordering for future PMA support.

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)

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) = {

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

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)